Memory abstraction.

8 files changed, 1086 insertions, 84 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 83797ec7..0ff564dc 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26581,6 +26581,7 @@ usage:
     Abc_Print( -2, "\t         a toolkit for constraint manipulation\n" );
     Abc_Print( -2, "\t         if constraints are absent, detect them functionally\n" );
     Abc_Print( -2, "\t         if constraints are present, profiles them using random simulation\n" );
+    Abc_Print( -2, "\t         (constraints fail when any of them becomes 1 in any timeframe)\n" );
     Abc_Print( -2, "\t-F num : the max number of timeframes to consider [default = %d]\n", nFrames );
     Abc_Print( -2, "\t-C num : the max number of conflicts in SAT solving [default = %d]\n", nConfs );
     Abc_Print( -2, "\t-P num : the max number of propagations in SAT solving [default = %d]\n", nProps );
@@ -26818,6 +26819,7 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     Abc_Print( -2, "usage: fold [-cvh]\n" );
     Abc_Print( -2, "\t         folds constraints represented as separate outputs\n" );
+    Abc_Print( -2, "\t         (constraints fail when any of them becomes 1 in any timeframe)\n" );
     Abc_Print( -2, "\t-c     : toggle complementing constraints while folding [default = %s]\n", fCompl? "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");
diff --git a/src/base/wlc/module.make b/src/base/wlc/module.make
index c722f6f3..1778622c 100644
--- a/src/base/wlc/module.make
+++ b/src/base/wlc/module.make
@@ -6,6 +6,7 @@ SRC +=    src/base/wlc/wlcAbs.c \
     src/base/wlc/wlcCom.c \
     src/base/wlc/wlcGraft.c \
     src/base/wlc/wlcJson.c \
+    src/base/wlc/wlcMem.c \
     src/base/wlc/wlcNdr.c \
     src/base/wlc/wlcNtk.c \
     src/base/wlc/wlcReadSmt.c \
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index dc58cc64..5498d9da 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -61,7 +61,7 @@ typedef enum {
     WLC_OBJ_BIT_AND,       // 16: bitwise AND
     WLC_OBJ_BIT_OR,        // 17: bitwise OR
     WLC_OBJ_BIT_XOR,       // 18: bitwise XOR
-    WLC_OBJ_BIT_NAND,      // 19: bitwise AND
+    WLC_OBJ_BIT_NAND,      // 19: bitwise NAND
     WLC_OBJ_BIT_NOR,       // 20: bitwise OR
     WLC_OBJ_BIT_NXOR,      // 21: bitwise NXOR
     WLC_OBJ_BIT_SELECT,    // 22: bit selection
@@ -161,6 +161,7 @@ struct Wlc_Ntk_t_
     Vec_Int_t              vBits;              // object mapping into AIG nodes
     Vec_Int_t              vLevels;            // object levels
     Vec_Int_t              vRefs;              // object reference counters
+    Vec_Int_t              vPoPairs;           // pairs of primary outputs
 };
 
 typedef struct Wlc_Par_t_ Wlc_Par_t;
@@ -364,6 +365,11 @@ extern int            Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
 extern Gia_Man_t *    Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pPars );
 /*=== wlcCom.c ========================================================*/
 extern void           Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk );
+/*=== wlcMem.c ========================================================*/
+extern Vec_Int_t *    Wlc_NtkCollectMemory( Wlc_Ntk_t * p );
+extern void           Wlc_NtkPrintMemory( Wlc_Ntk_t * p );
+extern Wlc_Ntk_t *    Wlc_NtkMemAbstractTest( Wlc_Ntk_t * p );
+extern int            Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fPdrVerbose, int fVerbose );
 /*=== wlcNdr.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_ReadNdr( char * pFileName );
 extern void           Wlc_WriteNdr( Wlc_Ntk_t * pNtk, char * pFileName );
@@ -380,6 +386,7 @@ extern void           Wlc_ObjSetCo( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int fFlopIn
 extern char *         Wlc_ObjName( Wlc_Ntk_t * p, int iObj );
 extern void           Wlc_ObjUpdateType( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int Type );
 extern void           Wlc_ObjAddFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins );
+extern int            Wlc_ObjDup( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * vFanins );
 extern void           Wlc_NtkFree( Wlc_Ntk_t * p );
 extern int            Wlc_NtkCreateLevels( Wlc_Ntk_t * p );
 extern int            Wlc_NtkCreateLevelsRev( Wlc_Ntk_t * p );
@@ -410,6 +417,7 @@ extern void           Wlc_NtkDeleteSim( Vec_Ptr_t * p );
 /*=== wlcStdin.c ========================================================*/
 extern int            Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd );
 /*=== wlcReadVer.c ========================================================*/
+extern char *         Wlc_PrsConvertInitValues( Wlc_Ntk_t * p );
 extern Wlc_Ntk_t *    Wlc_ReadVer( char * pFileName, char * pStr );
 /*=== wlcUif.c ========================================================*/
 extern Vec_Int_t *    Wlc_NtkCollectAddMult( Wlc_Ntk_t * p, Wlc_BstPar_t * pPar, int * pCountA, int * CountM );
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 2b453cbc..b8853dda 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -36,19 +36,19 @@ 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_CommandPdrAbs     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandAbs2       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandMemAbs     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandBlast      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandGraft      ( 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 );
 static int  Abc_CommandShow       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int  Abc_CommandTest       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
 static int  Abc_CommandInvPs      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandInvPrint   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandInvCheck   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandInvGet     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandInvPut     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandInvMin     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandTest       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc )                       { return (Wlc_Ntk_t *)pAbc->pAbcWlc;                      }
 static inline void        Wlc_AbcFreeNtk( Abc_Frame_t * pAbc )                      { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc));  }
@@ -80,6 +80,7 @@ void Wlc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Word level", "%abs",         Abc_CommandAbs,        0 );
     Cmd_CommandAdd( pAbc, "Word level", "%pdra",        Abc_CommandPdrAbs,     0 );
     Cmd_CommandAdd( pAbc, "Word level", "%abs2",        Abc_CommandAbs2,       0 );
+    Cmd_CommandAdd( pAbc, "Word level", "%memabs",      Abc_CommandMemAbs,     0 );
     Cmd_CommandAdd( pAbc, "Word level", "%blast",       Abc_CommandBlast,      0 );
     Cmd_CommandAdd( pAbc, "Word level", "%graft",       Abc_CommandGraft,      0 );
     Cmd_CommandAdd( pAbc, "Word level", "%profile",     Abc_CommandProfile,    0 );
@@ -305,11 +306,12 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fShowCones   = 0;
     int fShowMulti   = 0;
     int fShowAdder   = 0;
+    int fShowMem     = 0;
     int fDistrib     = 0;
     int fTwoSides    = 0;
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "cmadtvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cmardtvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -322,6 +324,9 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             fShowAdder ^= 1;
             break;
+        case 'r':
+            fShowMem ^= 1;
+            break;
         case 'd':
             fDistrib ^= 1;
             break;
@@ -349,16 +354,19 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
         Wlc_NtkPrintNodes( pNtk, WLC_OBJ_ARI_MULTI );
     if ( fShowAdder )
         Wlc_NtkPrintNodes( pNtk, WLC_OBJ_ARI_ADD );
+    if ( fShowMem )
+        Wlc_NtkPrintMemory( pNtk );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%ps [-cmadtvh]\n" );
+    Abc_Print( -2, "usage: %%ps [-cmardtvh]\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" );
     Abc_Print( -2, "\t-a     : toggle printing adders [default = %s]\n",                fShowAdder? "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-v     : toggle printing verbose information [default = %s]\n",   fVerbose? "yes": "no" );
+    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-v     : toggle printing verbose information [default = %s]\n",   fVerbose?   "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -885,6 +893,66 @@ usage:
   SeeAlso     []
 
 ******************************************************************************/
+int Abc_CommandMemAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    int c, nIterMax = 1000, fPdrVerbose = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Iwvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nIterMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nIterMax <= 0 )
+                goto usage;
+            break;
+        case 'w':
+            fPdrVerbose ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 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_NtkMemAbstract( pNtk, nIterMax, fPdrVerbose, fVerbose );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%memabs [-I num] [-wvh]\n" );
+    Abc_Print( -2, "\t         memory abstraction for word-level networks\n" );
+    Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n",  nIterMax );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w     : toggle printing verbose PDR output [default = %s]\n",  fPdrVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
 int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
@@ -1170,13 +1238,16 @@ int Abc_CommandShow( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Wlc_NtkShow( Wlc_Ntk_t * p, Vec_Int_t * vBold );
     Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
-    int c, fVerbose = 0;
+    int c, fMemory = 0, fVerbose = 0;
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'm':
+            fMemory ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -1189,70 +1260,25 @@ int Abc_CommandShow( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Empty network.\n" );
         return 1;
     }
-    Wlc_NtkShow( pNtk, NULL );
+    if ( fMemory )
+    {
+        Vec_Int_t * vTemp = Wlc_NtkCollectMemory( pNtk );
+        Wlc_NtkShow( pNtk, vTemp );
+        Vec_IntFree( vTemp );
+    }
+    else
+        Wlc_NtkShow( pNtk, NULL );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: %%show [-h]\n" );
-    Abc_Print( -2, "       visualizes the network structure using DOT and GSVIEW\n" );
+    Abc_Print( -2, "usage: %%show [-mh]\n" );
+    Abc_Print( -2, "          visualizes the network structure using DOT and GSVIEW\n" );
 #ifdef WIN32
-    Abc_Print( -2, "       \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
-    Abc_Print( -2, "       (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
+    Abc_Print( -2, "          \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
+    Abc_Print( -2, "          (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
 #endif
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function********************************************************************
-
-  Synopsis    []
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p );
-    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
-    int c, fVerbose  = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pNtk == NULL )
-    {
-        Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" );
-        return 0;
-    }
-    // transform
-    //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
-    //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
-    //Wlc_AbcUpdateNtk( pAbc, pNtk );
-    //Wlc_GenerateSmtStdout( pAbc );
-    //Wlc_NtkSimulateTest( (Wlc_Ntk_t *)pAbc->pAbcWlc );
-    //pNtk = Wlc_NtkDupSingleNodes( pNtk );
-    //Wlc_AbcUpdateNtk( pAbc, pNtk );
-    //Wlc_ReadNdrTest( pNtk );
-    return 0;
-usage:
-    Abc_Print( -2, "usage: %%test [-vh]\n" );
-    Abc_Print( -2, "\t         experiments with word-level networks\n" );
-    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");
+    Abc_Print( -2, "\t-m   :  toggle showing memory subsystem [default = %s]\n", fMemory? "yes": "no" );
+    Abc_Print( -2, "\t-h   :  print the command usage\n");
     return 1;
 }
 
@@ -1590,6 +1616,62 @@ usage:
     return 1;
 }
 
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p );
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" );
+        return 0;
+    }
+    // transform
+    //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
+    //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
+    //Wlc_AbcUpdateNtk( pAbc, pNtk );
+    //Wlc_GenerateSmtStdout( pAbc );
+    //Wlc_NtkSimulateTest( (Wlc_Ntk_t *)pAbc->pAbcWlc );
+    //pNtk = Wlc_NtkDupSingleNodes( pNtk );
+    //Wlc_AbcUpdateNtk( pAbc, pNtk );
+    //Wlc_ReadNdrTest( pNtk );
+    pNtk = Wlc_NtkMemAbstractTest( pNtk );
+    Wlc_AbcUpdateNtk( pAbc, pNtk );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%test [-vh]\n" );
+    Abc_Print( -2, "\t         experiments with word-level networks\n" );
+    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;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcMem.c b/src/base/wlc/wlcMem.c
new file mode 100644
index 00000000..52cb2e2d
--- /dev/null
+++ b/src/base/wlc/wlcMem.c
@@ -0,0 +1,821 @@
+/**CFile****************************************************************
+
+  FileName    [wlcMem.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Memory abstraction.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 22, 2014.]
+
+  Revision    [$Id: wlcMem.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wlc.h"
+#include "sat/bsat/satStore.h"
+#include "proof/pdr/pdr.h"
+#include "proof/pdr/pdrInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Collect memory nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkCollectMemSizes( Wlc_Ntk_t * p )
+{
+    Wlc_Obj_t * pObj; int i;
+    Vec_Int_t * vMemSizes = Vec_IntAlloc( 10 );
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        if ( Wlc_ObjType(pObj) != WLC_OBJ_WRITE && Wlc_ObjType(pObj) != WLC_OBJ_READ )
+            continue;
+        pObj = Wlc_ObjFanin( p, pObj, 0 );
+        Vec_IntPushUnique( vMemSizes, Wlc_ObjRange(pObj) );
+    }
+    return vMemSizes;
+}
+Vec_Int_t * Wlc_NtkCollectMemory( Wlc_Ntk_t * p )
+{
+    Wlc_Obj_t * pObj; int i;
+    Vec_Int_t * vMemSizes = Wlc_NtkCollectMemSizes( p );
+    Vec_Int_t * vMemObjs = Vec_IntAlloc( 10 );
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        if ( Wlc_ObjType(pObj) == WLC_OBJ_WRITE || Wlc_ObjType(pObj) == WLC_OBJ_READ )
+            Vec_IntPush( vMemObjs, i );
+        else if ( Vec_IntFind(vMemSizes, Wlc_ObjRange(pObj)) >= 0 )
+            Vec_IntPush( vMemObjs, i );
+    }
+    Vec_IntFree( vMemSizes );
+    return vMemObjs;
+}
+void Wlc_NtkPrintMemory( Wlc_Ntk_t * p )
+{
+    Vec_Int_t * vMemory;
+    vMemory = Wlc_NtkCollectMemSizes( p );
+    Vec_IntSort( vMemory, 0 );
+    Wlc_NtkPrintNodeArray( p, vMemory );
+    Vec_IntFree( vMemory );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect fanins of memory subsystem.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkCollectMemFanins( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs )
+{
+    Wlc_Obj_t * pObj; int i, k, iFanin;
+    Vec_Int_t * vMemFanins = Vec_IntAlloc( 100 );
+    Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i )
+    {
+        if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
+            Vec_IntPush( vMemFanins, Wlc_ObjFaninId0(pObj) );
+        else if ( Wlc_ObjType(pObj) == WLC_OBJ_READ || Wlc_ObjType(pObj) == WLC_OBJ_WRITE )
+        {
+            Wlc_ObjForEachFanin( pObj, iFanin, k )
+                if ( k > 0 )
+                    Vec_IntPush( vMemFanins, iFanin );
+        }
+    }
+    return vMemFanins;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Abstract memory nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Wlc_CountDcs( char * pInit )
+{
+    int Count = 0;
+    for ( ; *pInit; pInit++ )
+        Count += (*pInit == 'x' || *pInit == 'X');
+    return Count;
+}
+int Wlc_NtkDupOneObject( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int TypeNew, Vec_Int_t * vFanins )
+{
+    unsigned Type = pObj->Type;
+    int iObjNew, nFanins = Wlc_ObjFaninNum(pObj);
+    pObj->Type = TypeNew;
+    pObj->nFanins = 0;
+    iObjNew = Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+    pObj->Type = Type;
+    pObj->nFanins = (unsigned)nFanins;
+    if ( TypeNew == WLC_OBJ_FO )
+        Vec_IntPush( pNew->vInits, -Wlc_ObjRange(pObj) );
+    return iObjNew;
+}
+void Wlc_NtkDupOneBuffer( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins, int fIsFi )
+{
+    int iObj = Wlc_ObjAlloc( pNew, WLC_OBJ_BUF, pObj->Signed, pObj->End, pObj->Beg );
+    Wlc_Obj_t * pObjNew = Wlc_NtkObj( pNew, iObj );
+    Vec_IntFill( vFanins, 1, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)) );
+    Wlc_ObjAddFanins( pNew, pObjNew, vFanins );
+    Wlc_ObjSetCo( pNew, pObjNew, fIsFi );
+}
+
+void Wlc_NtkAbsAddToNodeFrames( Vec_Int_t * vNodeFrames, Vec_Int_t * vLevel ) 
+{
+    int i, Entry;
+    Vec_IntForEachEntry( vLevel, Entry, i )
+        Vec_IntPushUnique( vNodeFrames, Entry );
+    Vec_IntSort( vNodeFrames, 0 );
+}
+Vec_Int_t * Wlc_NtkAbsCreateFlopOutputs( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * vNodeFrames, Vec_Int_t * vFanins ) 
+{
+    Vec_Int_t * vNewObjs = Vec_IntAlloc( 2*Vec_IntSize(vNodeFrames) );
+    Wlc_Obj_t * pObj, * pFanin = NULL;
+    int i, Entry, iObj, iFrame;
+    Vec_IntForEachEntry( vNodeFrames, Entry, i )
+    {
+        iObj   = Entry >> 10;
+        iFrame = Entry & 0x3FF;
+        pObj   = Wlc_NtkObj( p, iObj );
+        // address
+        if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
+            pFanin = Wlc_ObjFanin0(p, pObj);
+        else if ( Wlc_ObjType(pObj) == WLC_OBJ_READ || Wlc_ObjType(pObj) == WLC_OBJ_WRITE )
+            pFanin = Wlc_ObjFanin1(p, pObj);
+        else assert( 0 );
+        Vec_IntPush( vNewObjs, Wlc_NtkDupOneObject(pNew, p, pFanin, WLC_OBJ_FO, vFanins) );
+        // data
+        if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
+            pFanin = NULL;
+        else if ( Wlc_ObjType(pObj) == WLC_OBJ_READ )
+            pFanin = pObj;
+        else if ( Wlc_ObjType(pObj) == WLC_OBJ_WRITE )
+            pFanin = Wlc_ObjFanin2(p, pObj);
+        else assert( 0 );
+        Vec_IntPush( vNewObjs, pFanin ? Wlc_NtkDupOneObject(pNew, p, pFanin, WLC_OBJ_FO, vFanins) : 0 );
+    }
+    assert( Vec_IntSize(vNewObjs) == Vec_IntCap(vNewObjs) );
+    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 ) 
+{
+    Vec_Int_t * vLevel; 
+    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 )
+    {
+        assert( Vec_IntSize(vLevel) >= 2 );
+        Vec_IntClear( vLevConstr );
+
+        Index[0] = Vec_IntFind( vNodeFrames, Vec_IntEntry(vLevel, 0) );
+        Index[1] = Vec_IntFind( vNodeFrames, Vec_IntEntryLast(vLevel) );
+        assert( Index[0] >= 0 && Index[1] >= 0 );
+
+        pAddrs[0] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[0]) );
+        pAddrs[1] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[1]) );
+
+        pDatas[0] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[0]+1) );
+        pDatas[1] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[1]+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]) );
+        Wlc_ObjAddFanins( pNew, pCond, vFanins );
+        Vec_IntPush( vLevConstr, Wlc_ObjId(pNew, pCond) );
+
+        // different datas
+        pCond = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_COMP_NOTEQU, 0, 0, 0));
+        Vec_IntFillTwo( vFanins, 2, Wlc_ObjId(pNew, pDatas[0]), Wlc_ObjId(pNew, pDatas[1]) );
+        Wlc_ObjAddFanins( pNew, pCond, vFanins );
+        Vec_IntPush( vLevConstr, Wlc_ObjId(pNew, pCond) );
+
+        Vec_IntForEachEntryStartStop( vLevel, Entry, k, 0, Vec_IntSize(vLevel)-1 )
+        {
+            Index[0]  = Vec_IntFind( vNodeFrames, Entry );            
+            pAddrs[0] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[0]) );
+            if ( Vec_IntEntry(vNewObjs, 2*Index[0]+1) == 0 ) // MUX
+                Vec_IntPush( vLevConstr, Wlc_ObjId(pNew, pAddrs[0]) );
+            else // different addresses
+            {
+                assert( Wlc_ObjRange(pAddrs[0]) == Wlc_ObjRange(pAddrs[1]) );
+                pCond = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_COMP_NOTEQU, 0, 0, 0));
+                Vec_IntFillTwo( vFanins, 2, Wlc_ObjId(pNew, pAddrs[0]), Wlc_ObjId(pNew, pAddrs[1]) );
+                Wlc_ObjAddFanins( pNew, pCond, vFanins );
+                Vec_IntPush( vLevConstr, Wlc_ObjId(pNew, pCond) );
+            }
+        }
+
+        // create last output
+        pConstr = Wlc_NtkObj( pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vLevConstr)-1, 0) );
+        Wlc_ObjAddFanins( pNew, pConstr, vLevConstr );
+        Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pConstr) );
+        pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_REDUCT_AND, 0, 0, 0));
+        Wlc_ObjAddFanins( pNew, pConstr, vFanins );
+
+        // save the result
+        Vec_IntPush( vBitConstr, Wlc_ObjId(pNew, pConstr) );
+    }
+    if ( Vec_IntSize(vBitConstr) > 0 )
+    {
+        // create last output
+        pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vBitConstr)-1, 0));
+        Wlc_ObjAddFanins( pNew, pConstr, vBitConstr );
+        // create last output
+        Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pConstr) );
+        pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_REDUCT_OR, 0, 0, 0));
+        Wlc_ObjAddFanins( pNew, pConstr, vFanins );
+    }
+    else
+    {
+        pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_CONST, 0, 0, 0));
+        Vec_IntFill( vFanins, 1, 0 ); // const0 - always true
+        Wlc_ObjAddFanins( pNew, pConstr, vFanins );
+    }
+    // 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 );
+        }
+    }
+}
+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 * pNew;
+    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;
+
+    // mark memory nodes
+    Wlc_NtkCleanMarks( p );
+    Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i )
+        pObj->Mark = 1;
+
+    // start new network
+    Wlc_NtkCleanCopy( p );
+    pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc + 1000 );
+    pNew->fSmtLib = p->fSmtLib;
+    pNew->vInits = Vec_IntAlloc( 100 );
+
+    // duplicate PIs
+    Wlc_NtkForEachPi( p, pObj, i )
+        if ( !pObj->Mark )
+        {
+            Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+            nBits += Wlc_ObjRange(pObj);
+        }
+
+    // create new PIs
+    *piFirstMemPi = nBits;
+    Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i )
+        if ( Wlc_ObjType(pObj) == WLC_OBJ_READ )
+        {
+            int iObjNew = Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_PI, vFanins );
+            nBits += Wlc_ObjRange(pObj);
+        }
+
+    // duplicate flop outputs
+    *piFirstCi = nBits;
+    Wlc_NtkForEachCi( p, pObj, i )
+        if ( !Wlc_ObjIsPi(pObj) && !pObj->Mark )
+        {
+            Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+            Vec_IntPush( pNew->vInits, Vec_IntEntry(p->vInits, i-Wlc_NtkPiNum(p)) );
+            nBits += Wlc_ObjRange(pObj);
+        }
+
+    // create flop for time-frame counter 
+    pCounter = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_FO, 0, AdderBits-1, 0));
+    Vec_IntPush( pNew->vInits, -AdderBits );
+    nBits += AdderBits;
+
+    // create flops for memory objects
+    *piFirstMemCi = nBits;
+    if ( vMemFanins )
+        Wlc_NtkForEachObjVec( vMemFanins, p, pObj, i )
+            Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_FO, vFanins );
+
+    // create flops for constraint objects
+    if ( vConstrs )
+        vNewObjs = Wlc_NtkAbsCreateFlopOutputs( pNew, p, vNodeFrames, vFanins );
+
+    // duplicate objects
+    Wlc_NtkForEachObj( p, pObj, i )
+        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
+        Vec_IntForEachEntryDouble( &p->vPoPairs, Po0, Po1, i )
+        {
+            int iCopy0 = Wlc_ObjCopy(p, Wlc_ObjId(p, Wlc_NtkPo(p, Po0)));
+            int iCopy1 = Wlc_ObjCopy(p, Wlc_ObjId(p, Wlc_NtkPo(p, Po1)));
+            int iObj = Wlc_ObjAlloc( pNew, WLC_OBJ_COMP_NOTEQU, 0, 0, 0 );
+            Wlc_Obj_t * pObjNew = Wlc_NtkObj( pNew, iObj );
+            Vec_IntFillTwo( vFanins, 1, iCopy0, iCopy1 );
+            Wlc_ObjAddFanins( pNew, pObjNew, vFanins );
+            Wlc_ObjSetCo( pNew, pObjNew, 0 );
+        }
+        printf( "Created %d miter outputs.\n", Wlc_NtkPoNum(pNew) );
+        Wlc_NtkForEachCo( p, pObj, i )
+            if ( pObj->fIsFi )
+                Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
+
+        // create constraint output
+        if ( vConstrs )
+            Wlc_ObjSetCo( pNew, pConstr, 0 );
+    }
+    else
+    {
+        // duplicate POs
+        Wlc_NtkForEachPo( p, pObj, i )
+            if ( !pObj->Mark )
+                Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
+        // create constraint output
+        if ( pConstr )
+            Wlc_ObjSetCo( pNew, pConstr, 0 );
+        // duplicate FIs
+        Wlc_NtkForEachCo( p, pObj, i )
+            if ( !Wlc_ObjIsPo(pObj) && !pObj->Mark )
+                Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
+    }
+
+    // create time-frame counter
+    pConst = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_CONST, 0, AdderBits-1, 0));
+    Vec_IntFill( vFanins, 1, 1 );
+    Wlc_ObjAddFanins( pNew, pConst, vFanins );
+
+    pAdder = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_ARI_ADD, 0, AdderBits-1, 0));
+    Vec_IntFillTwo( vFanins, 2, Wlc_ObjId(pNew, pCounter), Wlc_ObjId(pNew, pConst) );
+    Wlc_ObjAddFanins( pNew, pAdder, vFanins );
+    Wlc_ObjSetCo( pNew, pAdder, 1 );
+
+    // create new flop inputs
+    if ( vMemFanins )
+        Wlc_NtkForEachObjVec( vMemFanins, p, pObj, i )
+            Wlc_NtkDupOneBuffer( pNew, p, pObj, vFanins, 1 );
+
+    // create flop inputs for constraint objects
+    if ( vConstrs )
+        Wlc_NtkAbsCreateFlopInputs( pNew, p, vNodeFrames, vFanins, vNewObjs, pCounter, AdderBits, vMuxVal );
+
+    // append init states
+    pNew->pInits = Wlc_PrsConvertInitValues( pNew );
+    if ( p->pSpec )
+        pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    //Wlc_NtkTransferNames( pNew, p );
+    Vec_IntFree( vFanins );
+    Vec_IntFreeP( &vNewObjs );
+    Wlc_NtkCleanMarks( p );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives values of memory subsystem objects under the CEX.]
+
+  Description []
+               
+  SideEffects []
+
+  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 * 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;
+    Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i )
+    {
+        if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
+        {
+            //Vec_IntPush( vMemFanins, Wlc_ObjFaninId0(pObj) );
+            pFanin = Wlc_ObjFanin0(p, pObj);
+            assert( Wlc_ObjRange(pFanin) == 1 );
+            Vec_IntWriteEntry( vFirstTotal, 3*i, (iFirstMemCi << 10) | Wlc_ObjRange(pFanin) );
+            iFirstMemCi += Wlc_ObjRange(pFanin);
+            nMemFanins++;
+        }
+        else if ( Wlc_ObjType(pObj) == WLC_OBJ_READ || Wlc_ObjType(pObj) == WLC_OBJ_WRITE )
+        {
+            Wlc_ObjForEachFanin( pObj, iFanin, k )
+                if ( k > 0 )
+                {
+                    //Vec_IntPush( vMemFanins, iFanin );
+                    pFanin = Wlc_NtkObj(p, iFanin);
+                    Vec_IntWriteEntry( vFirstTotal, 3*i + k, (iFirstMemCi << 10) | Wlc_ObjRange(pFanin) );
+                    iFirstMemCi += Wlc_ObjRange(pFanin);
+                    nMemFanins++;
+                }
+            if ( Wlc_ObjType(pObj) == WLC_OBJ_READ )
+            {
+                Vec_IntWriteEntry( vFirstTotal, 3*i + 2, (iFirstMemPi << 10) | Wlc_ObjRange(pObj) );
+                iFirstMemPi += Wlc_ObjRange(pObj);
+            }
+        }
+    }
+    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 );
+    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
+    // assign primary inputs
+    Gia_ManForEachPi( pAbs, pObj, k )
+        pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
+    // simulate
+    Gia_ManForEachAnd( pAbs, pObj, k )
+        pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                       (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+    // transfer to combinational outputs
+    Gia_ManForEachCo( pAbs, pObj, k )
+        pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+    // transfer values to flop outputs
+    Gia_ManForEachRiRo( pAbs, pObjRi, pObjRo, k )
+        pObjRo->fMark0 = pObjRi->fMark0;
+    // at this point PIs and FOs area assigned according to this time-frame
+    // collect values
+    Vec_IntForEachEntry( vFirstTotal, Entry, k )
+    {
+        if ( Entry == 0 )
+        {
+            Vec_WrdPush( vRes, ~(word)0 );
+            continue;
+        }
+        First = Entry >> 10;
+        assert( First < Gia_ManCiNum(pAbs) );
+        nBits = Entry & 0x3FF;
+        assert( nBits <= 64 );
+        Value = 0;
+        for ( b = 0; b < nBits; b++ )
+            if ( Gia_ManCi(pAbs, First+b)->fMark0 )
+                Value |= ((word)1) << b;
+        Vec_WrdWriteEntry( vRes, Vec_IntSize(vFirstTotal)*iFrame + k, Value );
+    }
+    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 * vValues = Vec_WrdStartFull( Vec_IntSize(vFirstTotal) * (pCex->iFrame + 1) );
+    int f, nBits = pCex->nRegs;
+    Gia_ManCleanMark0(pAbs); // init FOs to zero
+    for ( f = 0; f <= pCex->iFrame; f++ )
+        nBits = Wlc_NtkCexResim( pAbs, pCex, vFirstTotal, nBits, vValues, f );
+    return vValues;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives refinement.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_NtkTrace_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int iFrame, Vec_Int_t * vMemObjs, Vec_Wrd_t * vValues, word ValueA, Vec_Int_t * vRes )
+{
+    int iObj = Wlc_ObjId(p, pObj);
+    int iNum = Wlc_ObjCopy( p, iObj );
+    assert( iObj == Vec_IntEntry(vMemObjs, iNum) );
+    assert( iFrame >= 0 );
+    if ( Wlc_ObjIsPi(pObj) ) 
+        Vec_IntPush( vRes, (iObj << 10) | iFrame );
+    else if ( Wlc_ObjIsCo(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 );
+    }
+    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 );
+    }
+    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 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 );
+    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 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 iNumFirst = Wlc_ObjCopy( p, iObjFirst );
+    int iIndFirst = 3*(iFrmFirst*Vec_IntSize(vMemObjs) + iNumFirst);
+    assert( Vec_IntSize(vTrace) >= 2 );
+    assert( iObjLast  == Vec_IntEntry(vMemObjs, iNumLast) );
+    assert( iObjFirst == Vec_IntEntry(vMemObjs, iNumFirst) );
+    pObjLast  = Wlc_NtkObj(p, iObjLast);
+    pObjFirst = Wlc_NtkObj(p, iObjFirst);
+    assert( Wlc_ObjType(pObjLast) == WLC_OBJ_READ );
+    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) );
+    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_Int_t * vTrace, * vTrace1, * vTrace2;
+    assert( 3 * nFrames * Vec_IntSize(vMemObjs) == Vec_WrdSize(vValues) );
+    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 );
+            if ( Wlc_NtkTraceCheckConfict( p, vTrace, vMemObjs, vValues ) )
+            {
+                Vec_WecFree( vTraces );
+                return vTrace;
+            }
+            Vec_WecPushLevel( vTraces );
+            Vec_IntAppend( Vec_WecEntryLast(vTraces), vTrace );
+            Vec_IntFree( vTrace );
+        }
+    }
+    // check if there are any common read addresses
+    Vec_WecForEachLevel( vTraces, vTrace1, i )
+    Vec_WecForEachLevelStop( vTraces, vTrace2, f, i )
+        if ( Vec_IntEntry(vTrace1, 0) == Vec_IntEntry(vTrace2, 0) )
+        {
+            int iObj1 = Vec_IntEntryLast(vTrace1);
+            int iNum1 = Wlc_ObjCopy( p, iObj1 );
+            int iObj2 = Vec_IntEntryLast(vTrace2);
+            int iNum2 = Wlc_ObjCopy( p, iObj2 );
+            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
+            {
+                vTrace = Vec_IntAlloc( 100 );
+                Vec_IntPush( vTrace, Vec_IntPop(vTrace1) );
+                Vec_IntForEachEntry( vTrace1, Entry, i )
+                    Vec_IntPushUnique( vTrace, Entry );
+                Vec_IntForEachEntry( vTrace2, Entry, i )
+                    Vec_IntPushUnique( vTrace, Entry );
+                Vec_WecFree( vTraces );
+                return vTrace;
+            }
+        }
+    Vec_WecFree( vTraces );
+    return NULL;
+}
+Vec_Bit_t * Wlc_NtkCollectMuxValues( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Wrd_t * vValues, int nFrames )
+{
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Wlc_Ntk_t * Wlc_NtkMemAbstractTest( Wlc_Ntk_t * p )
+{
+    int iFirstMemPi, iFirstCi, iFirstMemCi, nDcBits;
+    Vec_Int_t * vFirstTotal;
+    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 );
+    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;
+    Vec_Wec_t * vRefines = Vec_WecAlloc( 100 );
+    Vec_Int_t * vNodeFrames = Vec_IntAlloc( 100 );
+    Vec_Int_t * vMemObjs, * vMemFanins, * vFirstTotal, * vRefine; 
+    int RetValue, iFirstMemPi, iFirstCi, iFirstMemCi, nDcBits, nIters;
+
+    vMemObjs    = Wlc_NtkCollectMemory( p );
+    vMemFanins  = Wlc_NtkCollectMemFanins( p, vMemObjs );
+    pNewFull    = Wlc_NtkAbstractMemory( p, vMemObjs, vMemFanins, &iFirstMemPi, &iFirstCi, &iFirstMemCi, NULL, NULL, NULL );
+    nDcBits     = Wlc_CountDcs( pNewFull->pInits );
+    vFirstTotal = Wlc_NtkDeriveFirstTotal( p, vMemObjs, vMemFanins, iFirstMemPi, nDcBits + iFirstMemCi );
+
+    pAbsFull    = Wlc_NtkBitBlast( pNewFull, NULL );
+    assert( Gia_ManPiNum(pAbsFull) == iFirstCi + nDcBits );
+
+    // perform abstraction
+    for ( nIters = 1; nIters < 10000; nIters++ )
+    {
+        // set up parameters to run PDR
+        Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
+        Pdr_ManSetDefaultParams( pPdrPars );
+        pPdrPars->fUseAbs    = 0;   // use 'pdr -t'  (on-the-fly abstraction)
+        pPdrPars->fVerbose   = fVerbose;
+
+        // derive specific abstraction
+        pNew = Wlc_NtkAbstractMemory( p, vMemObjs, NULL, &iFirstMemPi, &iFirstCi, &iFirstMemCi, vRefines, vNodeFrames, vMuxVal );
+        pAbs = Wlc_NtkBitBlast( pNew, NULL );
+        Wlc_NtkFree( pNew );
+        // simplify the AIG
+        pAbs = Gia_ManSeqStructSweep( pTemp = pAbs, 1, 1, 0 );
+        Gia_ManStop( pTemp );
+
+        // try to prove abstracted GIA by converting it to AIG and calling PDR
+        pAig = Gia_ManToAigSimple( pAbs );
+        Gia_ManStop( pAbs );
+        RetValue = Pdr_ManSolve( pAig, pPdrPars );
+        pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
+        Aig_ManStop( pAig );
+
+        // check if proved or undecided
+        if ( pCex == NULL ) 
+        {
+            assert( RetValue );
+            break;
+        }
+
+        // analyze counter-example
+        Vec_BitFreeP( &vMuxVal );
+        vValues = Wlc_NtkConvertCex( p, vFirstTotal, pAbs, pCex );
+        vMuxVal = Wlc_NtkCollectMuxValues( p, vMemObjs, vValues, pCex->iFrame + 1 );
+        vRefine = Wlc_NtkFindConflict( p, vMemObjs, vValues, pCex->iFrame + 1 );
+        Vec_WrdFree( vValues );
+        Abc_CexFree( pCex ); // return CEX in the future
+        if ( vRefine == NULL )
+            break;
+
+        // save refinement for the future
+        Vec_WecPushLevel( vRefines );
+        Vec_IntAppend( Vec_WecEntryLast(vRefines), vRefine );
+        Wlc_NtkAbsAddToNodeFrames( vNodeFrames, vRefine );
+        Vec_IntFree( vRefine );
+    }
+    // cleanup
+    Wlc_NtkFree( pNew );
+    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" );
+    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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 7d3895a0..b65558e6 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -85,7 +85,9 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = {
     "sqrt",                // 51: integer square root
     "squar",               // 52: integer square
     "table",               // 53: bit table
-    NULL                   // 54: unused
+    "READ",                // 54: mem read port
+    "WRITE",               // 55: mem write port
+    NULL                   // 56: unused
 };
 
 char * Wlc_ObjTypeName( Wlc_Obj_t * p ) { return Wlc_Names[p->Type]; }
@@ -252,6 +254,7 @@ void Wlc_NtkFree( Wlc_Ntk_t * p )
         Mem_FlexStop( p->pMemFanin, 0 );
     if ( p->pMemTable )
         Mem_FlexStop( p->pMemTable, 0 );
+    ABC_FREE( p->vPoPairs.pArray );
     Vec_PtrFreeP( &p->vTables );
     ABC_FREE( p->vPis.pArray );
     ABC_FREE( p->vPos.pArray );
@@ -466,6 +469,8 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fTwoSides, int fVerbose )
              pObj->Type == WLC_OBJ_BIT_NOT     || pObj->Type == WLC_OBJ_LOGIC_NOT   || pObj->Type == WLC_OBJ_ARI_MINUS )
             Sign = Wlc_NtkPrintDistribMakeSign( Wlc_ObjSign(pObj), Wlc_ObjSign(Wlc_ObjFanin0(p, pObj)), 0 );
         // 2-input types (including MUX)
+        else if ( Wlc_ObjFaninNum(pObj) == 0 )
+            printf( "Object %d with name \"%s\" has type 0. Looks like it was declared by not defined...\n", i, Wlc_ObjName(p, i) );
         else if ( Wlc_ObjFaninNum(pObj) == 1 )
             Sign = Wlc_NtkPrintDistribMakeSign( Wlc_ObjSign(pObj), Wlc_ObjSign(Wlc_ObjFanin0(p, pObj)), 0 );
         else
@@ -620,6 +625,16 @@ 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" : " " );
+    if ( pObj->Type == WLC_OBJ_PI )
+    {
+        printf( "                          PI\n" );
+        return;
+    }
+    if ( pObj->Type == WLC_OBJ_FO )
+    {
+        printf( "                          FO\n" );
+        return;
+    }
     if ( pObj->Type == WLC_OBJ_CONST )
         printf( "                          " );
     else
@@ -914,6 +929,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 ( Vec_IntSize(&p->vPoPairs) )
+        Vec_IntAppend( &pNew->vPoPairs, &p->vPoPairs );
     return pNew;
 }
 Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index e1994794..42fab688 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -42,6 +42,7 @@ struct Wlc_Prs_t_
     Wlc_Ntk_t *            pNtk;
     Mem_Flex_t *           pMemTable;
     Vec_Ptr_t *            vTables;
+    Vec_Str_t *            vPoPairs;
     int                    nConsts;
     int                    nNonZero[4];
     int                    nNegative[4];
@@ -97,6 +98,7 @@ void Wlc_PrsStop( Wlc_Prs_t * p )
         Wlc_NtkFree( p->pNtk );
     if ( p->pMemTable )
         Mem_FlexStop( p->pMemTable, 0 );
+    Vec_StrFreeP( &p->vPoPairs );
     Vec_PtrFreeP( &p->vTables );
     Vec_IntFree( p->vLines );
     Vec_IntFree( p->vStarts );
@@ -235,6 +237,20 @@ int Wlc_PrsRemoveComments( Wlc_Prs_t * p )
         {
             if ( pCur + 5 < pEnd && pCur[2] == 'a' && pCur[3] == 'b' && pCur[4] == 'c' && pCur[5] == '2' )
                 pCur[0] = pCur[1] = pCur[2] = pCur[3] = pCur[4] = pCur[5] = ' ';
+            else if ( !strncmp(pCur + 3, "Pair:", 5) )
+            {
+                if ( p->vPoPairs == NULL )
+                    p->vPoPairs = Vec_StrAlloc( 100 );
+                for ( pNext = pCur + 9; *pNext != '\n'; pNext++ )
+                {
+                    if ( *pNext == ' ' )
+                        Vec_StrPush( p->vPoPairs, '\0' );
+                    else if ( *pNext != '\r' )
+                        Vec_StrPush( p->vPoPairs, *pNext );
+                }
+                if ( Vec_StrEntryLast(p->vPoPairs) != 0 )
+                    Vec_StrPush(p->vPoPairs, 0);
+            }
             else
             {
                 pNext = Wlc_PrsFindSymbol( pCur, '\n' );
@@ -507,7 +523,7 @@ static inline char * Wlc_PrsFindName( char * pStr, char ** ppPlace )
 {
     static char Buffer[WLV_PRS_MAX_LINE];
     char * pThis = *ppPlace = Buffer;
-    int fNotName = 1;
+    int fNotName = 1, Count = 0;
     pStr = Wlc_PrsSkipSpaces( pStr );
     if ( !Wlc_PrsIsChar(pStr) )
         return NULL;
@@ -518,9 +534,16 @@ static inline char * Wlc_PrsFindName( char * pStr, char ** ppPlace )
         if ( fNotName && !Wlc_PrsIsChar(pStr) )
             break;
         if ( *pStr == '\\' )
+        {
+            Count++;
             fNotName = 0;
+        }
         else if ( !fNotName && *pStr == ' ' )
-            fNotName = 1;
+        {
+            Count--;
+            if ( !Count )
+                fNotName = 1;
+        }
         *pThis++ = *pStr++;
     }
     *pThis = 0;
@@ -1008,6 +1031,25 @@ startword:
                 p->pNtk->pInits = Wlc_PrsConvertInitValues( p->pNtk );
                 //printf( "%s", p->pNtk->pInits );
             }
+            if ( p->vPoPairs )
+            {
+                assert( Vec_StrEntryLast(p->vPoPairs) == 0 );
+                Vec_StrPush( p->vPoPairs, 0 );
+                pName = Vec_StrArray(p->vPoPairs);
+                while ( *pName )
+                {
+                    Wlc_NtkForEachPo( p->pNtk, pObj, i )
+                        if ( !strcmp(Wlc_ObjName(p->pNtk, Wlc_ObjId(p->pNtk, pObj)), pName) )
+                        {
+                            Vec_IntPush( &p->pNtk->vPoPairs, i );
+                            break;
+                        }
+                    assert( i < Wlc_NtkPoNum(p->pNtk) );
+                    pName += strlen(pName) + 1;
+                }
+                assert( Vec_IntSize(&p->pNtk->vPoPairs) % 2 == 0 );
+                printf( "Finished parsing %d output pairs to be checked for equivalence.\n", Vec_IntSize(&p->pNtk->vPoPairs)/2 );
+            }
             break;
         }
         // these are read as part of the interface
@@ -1211,13 +1253,13 @@ startword:
             pObj = Wlc_NtkObj( p->pNtk, NameIdOut );
             Wlc_ObjUpdateType( p->pNtk, pObj, WLC_OBJ_FO );
             Vec_IntPush( &p->pNtk->vFfs, NameIdOut );
-            if ( nBits != Wlc_ObjRange(pObj) )
-                printf( "Warning!  Flop input has bit-width (%d) that differs from the flop declaration (%d)\n", Wlc_ObjRange(pObj), nBits );
+            //if ( nBits != Wlc_ObjRange(pObj) )
+            //    printf( "Warning!  Flop output \"%s\" has bit-width (%d) that differs from the flop declaration (%d)\n", Abc_NamStr(p->pNtk->pManName, NameIdOut), Wlc_ObjRange(pObj), nBits );
             // create flop input
             pObj = Wlc_NtkObj( p->pNtk, NameIdIn );
             Vec_IntPush( &p->pNtk->vFfs, NameIdIn );
-            if ( nBits != Wlc_ObjRange(pObj) )
-                printf( "Warning!  Flop output has bit-width (%d) that differs from the flop declaration (%d)\n", Wlc_ObjRange(pObj), nBits );
+            //if ( nBits != Wlc_ObjRange(pObj) )
+            //    printf( "Warning!  Flop input \"%s\" has bit-width (%d) that differs from the flop declaration (%d)\n", Abc_NamStr(p->pNtk->pManName, NameIdIn), Wlc_ObjRange(pObj), nBits );
             // save flop init value
             if ( NameId == -1 )
                 printf( "Initial value of flop \"%s\" is not specified. Zero is assumed.\n", Abc_NamStr(p->pNtk->pManName, NameIdOut) );
@@ -1225,11 +1267,13 @@ startword:
             {
                 pObj = Wlc_NtkObj( p->pNtk, NameId );
                 if ( nBits != Wlc_ObjRange(pObj) )
-                    printf( "Warning!  Flop init signal bit-width (%d) is different from the flop declaration (%d)\n", Wlc_ObjRange(pObj), nBits );
+                    printf( "Warning!  Flop init signal \"%s\" bit-width (%d) is different from the flop declaration (%d)\n", Abc_NamStr(p->pNtk->pManName, NameId), Wlc_ObjRange(pObj), nBits );
             }
             if ( p->pNtk->vInits == NULL )
                 p->pNtk->vInits = Vec_IntAlloc( 100 );
             Vec_IntPush( p->pNtk->vInits, NameId > 0 ? NameId : -nBits );
+            // printf( "Created flop %s with range %d and init value %d (nameId = %d)\n", 
+            //     Abc_NamStr(p->pNtk->pManName, NameIdOut), Wlc_ObjRange(pObj), nBits, NameId );
         }
         else if ( Wlc_PrsStrCmp( pStart, "CPL_MEM_" ) )
         {
@@ -1277,6 +1321,7 @@ startword:
             Vec_IntPush( p->vFanins, NameAddr );
             if ( !fRead )
                 Vec_IntPush( p->vFanins, NameDi );
+            //printf( "Memory %s ", fRead ? "Read" : "Write" ); printf( "Fanins: " );  Vec_IntPrint( p->vFanins );
             Wlc_ObjAddFanins( p->pNtk, pObj, p->vFanins );
         }
         else if ( pStart[0] == '(' && pStart[1] == '*' ) // skip comments
@@ -1326,8 +1371,11 @@ Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr )
     if ( !Wlc_PrsDerive( p ) )
         goto finish;
     // derive topological order
-    pNtk = Wlc_NtkDupDfs( p->pNtk, 0, 1 );
-    pNtk->pSpec = Abc_UtilStrsav( pFileName );
+    if ( p->pNtk )
+    {
+        pNtk = Wlc_NtkDupDfs( p->pNtk, 0, 1 );
+        pNtk->pSpec = Abc_UtilStrsav( pFileName );
+    }
 finish:
     Wlc_PrsPrintErrorMessage( p );
     Wlc_PrsStop( p );
diff --git a/src/base/wlc/wlcShow.c b/src/base/wlc/wlcShow.c
index 1601d602..e64e9204 100644
--- a/src/base/wlc/wlcShow.c
+++ b/src/base/wlc/wlcShow.c
@@ -49,7 +49,7 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
     Wlc_Obj_t * pNode;
     int LevelMax, Prev, Level, i;
 
-    if ( Wlc_NtkObjNum(p) > 2000 )
+    if ( vBold ? (Vec_IntSize(vBold) > 2000) : (Wlc_NtkObjNum(p) > 2000) )
     {
         fprintf( stdout, "Cannot visualize WLC with more than %d nodes.\n", 2000 );
         return;
@@ -159,6 +159,8 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
     // generate the CO nodes
     Wlc_NtkForEachCo( p, pNode, i )
     {
+        if ( vBold && !pNode->Mark )
+            continue;
         pNode = Wlc_ObjCo2PoFo(p, i);
         fprintf( pFile, "  NodePo%d [label = \"%s_in %d\"", Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) ); 
         fprintf( pFile, ", shape = %s", i < Wlc_NtkPoNum(p) ? "invtriangle" : "box" );
@@ -180,11 +182,20 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
         {
             if ( (int)Wlc_ObjLevel(p, pNode) != Level )
                 continue;
+            if ( vBold && !pNode->Mark )
+                continue;
 
             if ( pNode->Type == WLC_OBJ_CONST )
             {
-                fprintf( pFile, "  Node%d [label = \"0x", i ); 
-                Abc_TtPrintHexArrayRev( pFile, (word *)Wlc_ObjConstValue(pNode), (Wlc_ObjRange(pNode) + 3) / 4 );
+                //char * pName = Wlc_ObjName(p, i);
+                fprintf( pFile, "  Node%d [label = \"%d\'h", i, Wlc_ObjRange(pNode) ); 
+                if ( Wlc_ObjRange(pNode) > 64 )
+                {
+                    Abc_TtPrintHexArrayRev( pFile, (word *)Wlc_ObjConstValue(pNode), 16 );
+                    fprintf( pFile, "..." );
+                }
+                else
+                    Abc_TtPrintHexArrayRev( pFile, (word *)Wlc_ObjConstValue(pNode), (Wlc_ObjRange(pNode) + 3) / 4 );
                 fprintf( pFile, "\"" ); 
             }
             else if ( pNode->Type == WLC_OBJ_BUF || pNode->Type == WLC_OBJ_MUX )
@@ -224,6 +235,8 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
     // generate the CI nodes
     Wlc_NtkForEachCi( p, pNode, i )
     {
+        if ( vBold && !pNode->Mark )
+            continue;
         fprintf( pFile, "  Node%d [label = \"%s %d\"", Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) ); 
         fprintf( pFile, ", shape = %s", i < Wlc_NtkPiNum(p) ? "triangle" : "box" );
         fprintf( pFile, ", color = coral, fillcolor = coral" );
@@ -237,6 +250,8 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
     fprintf( pFile, "title1 -> title2 [style = invis];\n" );
     Wlc_NtkForEachCo( p, pNode, i )
     {
+        if ( vBold && !pNode->Mark )
+            continue;
         pNode = Wlc_ObjCo2PoFo( p, i );
         fprintf( pFile, "title2 -> NodePo%d [style = invis];\n", Wlc_ObjId(p, pNode) );
     }
@@ -245,7 +260,9 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
     Wlc_NtkForEachCo( p, pNode, i )
     {
         pNode = Wlc_ObjCo2PoFo( p, i );
-        if ( i > 0 )
+        if ( vBold && !pNode->Mark )
+            continue;
+        if ( Prev >= 0 )
             fprintf( pFile, "NodePo%d -> NodePo%d [style = invis];\n", Prev, Wlc_ObjId(p, pNode) );
         Prev = Wlc_ObjId(p, pNode);
     }
@@ -253,7 +270,9 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
     Prev = -1;
     Wlc_NtkForEachCi( p, pNode, i )
     {
-        if ( i > 0 )
+        if ( vBold && !pNode->Mark )
+            continue;
+        if ( Prev >= 0 )
             fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Wlc_ObjId(p, pNode) );
         Prev = Wlc_ObjId(p, pNode);
     }
@@ -261,6 +280,8 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
     // generate edges
     Wlc_NtkForEachCo( p, pNode, i )
     {
+        if ( vBold && !pNode->Mark )
+            continue;
         fprintf( pFile, "NodePo%d",  Wlc_ObjId(p, Wlc_ObjCo2PoFo(p, i)) );
         fprintf( pFile, " -> " );
         fprintf( pFile, "Node%d",  Wlc_ObjId(p, pNode) );
@@ -274,6 +295,8 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
         int k, iFanin;
         if ( Wlc_ObjIsCi(pNode) )
             continue;
+        if ( vBold && !pNode->Mark )
+            continue;
         // generate the edge from this node to the next
         Wlc_ObjForEachFanin( pNode, iFanin, k )
         {