Experiments with memory abstraction.

9 files changed, 549 insertions, 11 deletions

diff --git a/abclib.dsp b/abclib.dsp
index d06292d5..512592e0 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1119,6 +1119,10 @@ SOURCE=.\src\base\wln\wln.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\wln\wlnMem.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\wln\wlnNdr.c
 # End Source File
 # Begin Source File
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 279ec6a2..bb134757 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -120,6 +120,7 @@ struct Wlc_Obj_t_ // 24 bytes
     unsigned               Type    :  6;       // node type
     unsigned               Signed  :  1;       // signed
     unsigned               Mark    :  1;       // user mark
+    unsigned               Mark2   :  1;       // user mark
     unsigned               fIsPo   :  1;       // this is PO
     unsigned               fIsFi   :  1;       // this is FI
     unsigned               fXConst :  1;       // this is X-valued constant
@@ -283,6 +284,10 @@ static inline int          Wlc_ObjIsPi( Wlc_Obj_t * p )
 static inline int          Wlc_ObjIsPo( Wlc_Obj_t * p )                             { return p->fIsPo;                                                         }
 static inline int          Wlc_ObjIsCi( Wlc_Obj_t * p )                             { return p->Type == WLC_OBJ_PI || p->Type == WLC_OBJ_FO;                   }
 static inline int          Wlc_ObjIsCo( Wlc_Obj_t * p )                             { return p->fIsPo || p->fIsFi;                                             }
+static inline int          Wlc_ObjIsRead( Wlc_Obj_t * p )                           { return p->Type == WLC_OBJ_READ;                                          }
+static inline int          Wlc_ObjIsWrite( Wlc_Obj_t * p )                          { return p->Type == WLC_OBJ_WRITE;                                         }
+static inline int          Wlc_ObjIsMux( Wlc_Obj_t * p )                            { return p->Type == WLC_OBJ_MUX;                                           }
+static inline int          Wlc_ObjIsBuf( Wlc_Obj_t * p )                            { return p->Type == WLC_OBJ_BUF;                                           }
 static inline int          Wlc_ObjIsFf( Wlc_Ntk_t * p, int i )                      { return Wlc_NtkObj(p, i)->Type == WLC_OBJ_FF;                             }
 
 static inline int          Wlc_ObjId( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )             { return pObj - p->pObjs;                                                  }
@@ -383,6 +388,7 @@ extern Vec_Int_t *    Wlc_NtkCollectMemory( Wlc_Ntk_t * p, int fClean );
 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 fDumpAbs, int fPdrVerbose, int fVerbose );
+extern Wlc_Ntk_t *    Wlc_NtkAbstractMem( Wlc_Ntk_t * p, int nFrames, int fVerbose );
 /*=== wlcNdr.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_ReadNdr( char * pFileName );
 extern void           Wlc_WriteNdr( Wlc_Ntk_t * pNtk, char * pFileName );
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index aa10c6af..3398bfa1 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -1267,8 +1267,8 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
     // blast in the topological order
     Wlc_NtkForEachObj( p, pObj, i )
     {
-//        char * pName1 = Wlc_ObjName(p, i);
-//        char * pName2 = Wlc_ObjFaninNum(pObj) ? Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) : NULL;
+        //char * pName1 = Wlc_ObjName(p, i);
+        //char * pName2 = Wlc_ObjFaninNum(pObj) ? Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) : NULL;
 
         nAndPrev = Gia_ManAndNum(pNew);
         nRange  = Wlc_ObjRange( pObj );
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index d785caf0..ad41d000 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -38,6 +38,7 @@ 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_CommandMemAbs2    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandBlast      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandBlastMem   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandGraft      ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -84,6 +85,7 @@ void Wlc_Init( Abc_Frame_t * pAbc )
     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", "%memabs2",     Abc_CommandMemAbs2,    0 );
     Cmd_CommandAdd( pAbc, "Word level", "%blast",       Abc_CommandBlast,      0 );
     Cmd_CommandAdd( pAbc, "Word level", "%blastmem",    Abc_CommandBlastMem,   0 );
     Cmd_CommandAdd( pAbc, "Word level", "%graft",       Abc_CommandGraft,      0 );
@@ -942,7 +944,7 @@ int Abc_CommandMemAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pNtk == NULL )
     {
-        Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
+        Abc_Print( 1, "Abc_CommandMemAbs(): There is no current design.\n" );
         return 0;
     }
     Wlc_NtkMemAbstract( pNtk, nIterMax, fDumpAbs, fPdrVerbose, fVerbose );
@@ -969,6 +971,63 @@ usage:
   SeeAlso     []
 
 ******************************************************************************/
+int Abc_CommandMemAbs2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    int c, nFrames = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames <= 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandMemAbs2(): There is no current design.\n" );
+        return 0;
+    }
+    pNtk = Wlc_NtkAbstractMem( pNtk, nFrames, fVerbose );
+    Wlc_AbcUpdateNtk( pAbc, pNtk );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%memabs2 [-F num] [-vh]\n" );
+    Abc_Print( -2, "\t         memory abstraction for word-level networks\n" );
+    Abc_Print( -2, "\t-F num : the number of timeframes [default = %d]\n",  nFrames );
+    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;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
 int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Wlc_NtkPrintInputInfo( Wlc_Ntk_t * pNtk );
@@ -1810,8 +1869,9 @@ usage:
 ******************************************************************************/
 int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    extern void Wlc_NtkExploreMem( Wlc_Ntk_t * p, int nFrames );
     extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p );
-    //Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@@ -1845,6 +1905,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     //pNtk = Wlc_NtkMemAbstractTest( pNtk );
     //Wlc_AbcUpdateNtk( pAbc, pNtk );
     //Wln_NtkFromWlcTest( pNtk );
+    Wlc_NtkExploreMem( pNtk, 0 );
     return 0;
 usage:
     Abc_Print( -2, "usage: %%test [-vh]\n" );
diff --git a/src/base/wlc/wlcMem.c b/src/base/wlc/wlcMem.c
index b61ddad0..09b7312b 100644
--- a/src/base/wlc/wlcMem.c
+++ b/src/base/wlc/wlcMem.c
@@ -309,11 +309,11 @@ int Wlc_NtkDupOneObject( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int
     }
     return iObjNew;
 }
-void Wlc_NtkDupOneBuffer( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins, int fIsFi )
+void Wlc_NtkDupOneBuffer( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int iFanin, 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)) );
+    Vec_IntFill( vFanins, 1, iFanin );
     Wlc_ObjAddFanins( pNew, pObjNew, vFanins );
     Wlc_ObjSetCo( pNew, pObjNew, fIsFi );
 }
@@ -593,9 +593,9 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_
             Wlc_ObjAddFanins( pNew, pObjNew, vFanins );
             Wlc_ObjSetCo( pNew, pObjNew, 0 );
         }
-        printf( "Created %d miter outputs.\n", Wlc_NtkPoNum(pNew) );
+        printf( "Memory abstraction created %d miter outputs.\n", Wlc_NtkPoNum(pNew) );
         Wlc_NtkForEachCo( p, pObj, i )
-            if ( pObj->fIsFi )
+            if ( pObj->fIsFi && !pObj->Mark )
                 Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
 
         // create constraint output
@@ -630,7 +630,7 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_
     // create new flop inputs
     if ( vMemFanins )
         Wlc_NtkForEachObjVec( vMemFanins, p, pObj, i )
-            Wlc_NtkDupOneBuffer( pNew, p, pObj, vFanins, 1 );
+            Wlc_NtkDupOneBuffer( pNew, p, pObj, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)), vFanins, 1 );
 
     // create flop inputs for constraint objects
     if ( vConstrs )
@@ -1096,6 +1096,420 @@ int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fDumpAbs, int fPdrVerbo
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Collect visited objects.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Wlc_NtkExploreMem2_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vCollect, int nFrames )
+{
+    int k, iFanin, nVisited = 0;
+    if ( pObj->Mark == 0 )
+        return 0;
+    if ( Wlc_ObjType(pObj) == WLC_OBJ_PI || (Wlc_ObjType(pObj) == WLC_OBJ_FO && nFrames == 0) )
+    {
+        Vec_IntPushTwo( vCollect, Wlc_ObjId(p, pObj), nFrames );
+        return 1;
+    }
+    if ( Wlc_ObjType(pObj) == WLC_OBJ_FO )
+        return Wlc_NtkExploreMem2_rec( p, Wlc_ObjFo2Fi(p, pObj), vCollect, nFrames-1 );
+    Wlc_ObjForEachFanin( pObj, iFanin, k )
+        nVisited += Wlc_NtkExploreMem2_rec( p, Wlc_NtkObj(p, iFanin), vCollect, nFrames );
+    Vec_IntPushTwo( vCollect, Wlc_ObjId(p, pObj), nFrames );
+    return nVisited + 1;
+}
+void Wlc_NtkExploreMem2( Wlc_Ntk_t * p, int nFrames )
+{
+    Wlc_Obj_t * pObj; int i, k, Entry, Frame, nVisited;
+    Vec_Int_t * vCollect = Vec_IntStart( 1000 );
+    Vec_Int_t * vMemObjsClean = Wlc_NtkCollectMemory( p, 1 );
+    Wlc_NtkCleanMarks( p );
+    Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
+        pObj->Mark = 1;
+    Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
+    {
+        if ( Wlc_ObjType(pObj) != WLC_OBJ_READ )
+            continue;
+        Vec_IntClear( vCollect );
+        nVisited = Wlc_NtkExploreMem2_rec( p, pObj, vCollect, nFrames );
+        printf( "Obj %6d : ", Wlc_ObjId(p, pObj) );
+        printf( "Visit = %6d  ", nVisited );
+        printf( "Pair = %6d  ", Vec_IntSize(vCollect)/2 );
+        if ( Vec_IntSize(vCollect)/2 < 10 )
+            Vec_IntForEachEntryDouble( vCollect, Entry, Frame, k )
+                printf( "%d(%d) ", Entry, Frame );
+        printf( "\n" );
+    }
+    Vec_IntFree( vMemObjsClean );
+    Vec_IntFree( vCollect );
+    Wlc_NtkCleanMarks( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect memory flops reachable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_NtkExploreMem_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vCollect, int nFrames )
+{
+    int k, iFanin;
+    if ( pObj->Mark == 0 )
+        return;
+    if ( Wlc_ObjType(pObj) == WLC_OBJ_PI || (Wlc_ObjType(pObj) == WLC_OBJ_FO && nFrames == 0) )
+    {
+        Vec_IntPushUnique( vCollect, Wlc_ObjId(p, pObj) );
+        return;
+    }
+    if ( Wlc_ObjType(pObj) == WLC_OBJ_FO )
+    {
+        Wlc_NtkExploreMem_rec( p, Wlc_ObjFo2Fi(p, pObj), vCollect, nFrames-1 );
+        return;
+    }
+    Wlc_ObjForEachFanin( pObj, iFanin, k )
+        Wlc_NtkExploreMem_rec( p, Wlc_NtkObj(p, iFanin), vCollect, nFrames );
+}
+void Wlc_NtkExploreMem( Wlc_Ntk_t * p, int nFrames )
+{
+    Wlc_Obj_t * pObj; int i, k, iObj;
+    Vec_Int_t * vCollect = Vec_IntStart( 1000 );
+    Vec_Int_t * vMemObjsClean = Wlc_NtkCollectMemory( p, 1 );
+    Wlc_NtkCleanMarks( p );
+    Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
+        pObj->Mark = 1;
+    Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
+    {
+        if ( Wlc_ObjType(pObj) != WLC_OBJ_READ )
+            continue;
+        Vec_IntClear( vCollect );
+        Wlc_NtkExploreMem_rec( p, pObj, vCollect, nFrames );
+        printf( "Read port %6d : ", Wlc_ObjId(p, pObj) );
+        printf( "Inputs = %6d  ", Vec_IntSize(vCollect) );
+        Vec_IntForEachEntry( vCollect, iObj, k )
+            printf( "%d(%s) ", iObj, Wlc_ObjName(p, iObj) );
+        printf( "\n" );
+    }
+    Vec_IntFree( vMemObjsClean );
+    Vec_IntFree( vCollect );
+    Wlc_NtkCleanMarks( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [For each READ find reachable CIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkFindReachablePiFo( Wlc_Ntk_t * p, Vec_Int_t * vMemObjsClean, int nFrames )
+{
+    Vec_Int_t * vRes = Vec_IntAlloc( 100 );
+    Wlc_Obj_t * pObjR, * pObjI, * pObj; 
+    int i, j, k, f, fFanin;
+    Wlc_NtkForEachObj( p, pObj, i )
+        pObj->Mark2 = 0;
+    // go through read ports
+    Wlc_NtkForEachObjVec( vMemObjsClean, p, pObjR, i ) if ( Wlc_ObjIsRead(pObjR) )
+    {
+        // go through memory CIs
+        Wlc_NtkForEachObjVec( vMemObjsClean, p, pObjI, j ) if ( Wlc_ObjIsCi(pObjI) )
+        {
+            // propagate bit from CI to READ
+            pObjI->Mark2 = 1;
+            Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, k )
+            {
+                if ( pObj == pObjI )
+                    continue;
+                assert( pObj->Mark2 == 0 );
+                Wlc_ObjForEachFanin( pObj, fFanin, f )
+                    pObj->Mark2 |= Wlc_NtkObj(p, fFanin)->Mark2;
+            }
+            if ( pObjR->Mark2 )
+                Vec_IntPushThree( vRes, Wlc_ObjId(p, pObjR), Wlc_ObjId(p, pObjI), -1 );
+            Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, k )
+                pObj->Mark2 = 0;
+        }
+    }
+    Wlc_NtkForEachObj( p, pObj, i )
+        assert( pObj->Mark2 == 0 );
+    return vRes;
+}
+Vec_Int_t * Wlc_NtkExtractCisForThisRead( Vec_Int_t * vReachReadCi, int iRead )
+{
+    int k;
+    Vec_Int_t * vRes = Vec_IntAlloc( 100 );
+    for ( k = 0; k < Vec_IntSize(vReachReadCi)/3; k++ )
+    {
+        if ( iRead != Vec_IntEntry( vReachReadCi, 3*k ) )
+            continue;
+        Vec_IntPush( vRes, Vec_IntEntry( vReachReadCi, 3*k+1 ) );
+        Vec_IntPush( vRes, Vec_IntEntry( vReachReadCi, 3*k+2 ) );
+    }
+    return vRes;
+}
+Vec_Int_t * Wlc_NtkCollectOneType( Wlc_Ntk_t * p, Vec_Int_t * vMemObjsClean, int Type1, int Type2 )
+{
+    Wlc_Obj_t * pObj; int i;
+    Vec_Int_t * vRes = Vec_IntAlloc( 100 );
+    Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
+        if ( Wlc_ObjType(pObj) == Type1 || Wlc_ObjType(pObj) == Type2 )
+            Vec_IntPush( vRes, Wlc_ObjId(p, pObj) );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create memory constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_NtkCreateMemoryConstr( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * vMemObjsClean, Vec_Int_t * vReachReadCi )
+{
+    Vec_Int_t * vReads  = Wlc_NtkCollectOneType( p, vMemObjsClean, WLC_OBJ_READ, -1 );
+    Vec_Int_t * vObjCis = Wlc_NtkCollectOneType( p, vMemObjsClean, WLC_OBJ_PI, WLC_OBJ_FO );
+    Vec_Int_t * vFanins = Vec_IntAlloc( 10 );
+    Wlc_Obj_t * pObjR, * pObj, * pCond; 
+    int i, k, iObjCi, iObjNew = -1;
+    // go through read ports
+    Wlc_NtkForEachObjVec( vReads, p, pObjR, i )
+    {
+        // ABC_READ  ( .mem_in(mem_fi1), .addr(raddr), .data(read1) ) ;
+        // ABC_WRITE ( .mem_in(mem_fo1), .addr(waddr), .data(data), .mem_out(mem_fi1) ) ;
+        // initialize CI related to the read port
+        Vec_Int_t * vLocalCis = Wlc_NtkExtractCisForThisRead( vReachReadCi, Wlc_ObjId(p, pObjR) );
+        Wlc_NtkForEachObjVec( vObjCis, p, pObj, k )
+            Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), -1 );
+        Vec_IntForEachEntryDouble( vLocalCis, iObjCi, iObjNew, k )
+            Wlc_ObjSetCopy( p, iObjCi, iObjNew );
+        Vec_IntFree( vLocalCis );
+        // implement the nodes
+        Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, k )
+        {
+            if ( Wlc_ObjIsRead(pObj) || Wlc_ObjIsCi(pObj) )
+                continue;
+            Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), -1 );
+            if ( Wlc_ObjIsWrite(pObj) )
+            {
+                if ( Wlc_ObjCopy(p, Wlc_ObjFaninId0(pObj)) == -1 )
+                    continue;
+                if ( Wlc_ObjRange(pObjR) != Wlc_ObjRange(Wlc_ObjFanin2(p, pObj)) )
+                    continue;
+                // create equality
+                pCond = Wlc_NtkObj( pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_COMP_EQU, 0, 0, 0) );
+                Vec_IntFillTwo( vFanins, 2, Wlc_ObjCopy(p, Wlc_ObjFaninId1(pObjR)), Wlc_ObjCopy(p, Wlc_ObjFaninId1(pObj)) );
+                //printf( "%d : ", Wlc_ObjId(p,pObj) ), Vec_IntPrint( vFanins );
+                Wlc_ObjAddFanins( pNew, pCond, vFanins );
+                // create MUX
+                iObjNew = Wlc_ObjAlloc( pNew, WLC_OBJ_MUX, 0, Wlc_ObjRange(pObjR)-1, 0 );
+                Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pCond) );
+                Vec_IntPush( vFanins, Wlc_ObjCopy(p, Wlc_ObjFaninId2(pObj)) );
+                Vec_IntPush( vFanins, Wlc_ObjCopy(p, Wlc_ObjFaninId0(pObj)) );
+                Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObjNew), vFanins );
+            }
+            else if ( Wlc_ObjIsMux(pObj) )
+            {
+                int iFanin0New = Wlc_ObjCopy(p, Wlc_ObjFaninId1(pObj));
+                int iFanin1New = Wlc_ObjCopy(p, Wlc_ObjFaninId2(pObj));
+                if ( iFanin0New == -1 || iFanin1New == -1 )
+                    continue;
+                //Wlc_NtkPrintNode( pNew, Wlc_NtkObj(pNew, iFanin0New) );
+                assert( Wlc_ObjRange(pObjR) == Wlc_ObjRange(Wlc_NtkObj(pNew, iFanin0New)) );
+                assert( Wlc_ObjRange(pObjR) == Wlc_ObjRange(Wlc_NtkObj(pNew, iFanin1New)) );
+                iObjNew = Wlc_ObjAlloc( pNew, WLC_OBJ_MUX, 0, Wlc_ObjRange(pObjR)-1, 0 );
+                Vec_IntFill( vFanins, 1, Wlc_ObjCopy(p, Wlc_ObjFaninId0(pObj)) );
+                Vec_IntPush( vFanins, iFanin0New );
+                Vec_IntPush( vFanins, iFanin1New );
+                Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObjNew), vFanins );
+            }
+            else if ( Wlc_ObjIsBuf(pObj) )
+            {
+                iObjNew = Wlc_ObjCopy( p, Wlc_ObjFaninId0(pObj) );
+                if ( iObjNew == -1 )
+                    continue;
+            }
+            else assert( 0 );
+            Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), iObjNew );
+        }
+        // extract fanin
+        iObjNew = Wlc_ObjCopy( p, Wlc_ObjFaninId0(pObjR) );
+        assert( iObjNew != -1 );
+        Vec_IntFill( vFanins, 1, iObjNew );
+        // add it as buffer fanin
+        iObjNew = Wlc_ObjCopy( p, Wlc_ObjId(p, pObjR) );
+        assert( Wlc_NtkObj(pNew, iObjNew)->Type == WLC_OBJ_BUF );
+        Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObjNew), vFanins );
+    }
+    Wlc_NtkForEachObjVec( vObjCis, p, pObj, k )
+        Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), -1 );
+    Vec_IntFree( vFanins );
+    Vec_IntFree( vReads );
+    Vec_IntFree( vObjCis );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Wlc_Ntk_t * Wlc_NtkAbstractMem( Wlc_Ntk_t * p, int nFrames, int fVerbose )
+{
+    Vec_Int_t * vMemObjsAll   = Wlc_NtkCollectMemory( p, 0 );
+    Vec_Int_t * vMemObjsClean = Wlc_NtkCollectMemory( p, 1 );
+    Vec_Int_t * vReachReadCi  = Wlc_NtkFindReachablePiFo( p, vMemObjsClean, nFrames );
+    Wlc_Ntk_t * pNew, * pTemp;
+    Wlc_Obj_t * pObj;
+    Vec_Int_t * vFanins  = Vec_IntAlloc( 100 );
+    int i, Po0, Po1, iObjNew;
+
+    assert( nFrames == 0 );
+
+    // mark memory nodes
+    Wlc_NtkCleanMarks( p );
+    Wlc_NtkForEachObjVec( vMemObjsAll, p, pObj, i )
+        pObj->Mark = 1;
+
+    // start new network
+    Wlc_NtkCleanCopy( p );
+    pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc + Vec_IntSize(vMemObjsClean) * nFrames * 10 );
+    pNew->fSmtLib   = p->fSmtLib;
+    pNew->fMemPorts = p->fMemPorts;
+    pNew->fEasyFfs  = p->fEasyFfs;
+    pNew->vInits    = Vec_IntAlloc( 100 );
+
+    // duplicate PIs
+    Wlc_NtkForEachPi( p, pObj, i )
+        if ( !pObj->Mark )
+            Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+
+    // create new PIs
+    assert( Vec_IntSize(vReachReadCi) % 3 == 0 );
+    for ( i = 0; i < Vec_IntSize(vReachReadCi)/3; i++ )
+    {
+        pObj = Wlc_NtkObj( p, Vec_IntEntry( vReachReadCi, 3*i ) );
+        assert( Wlc_ObjIsRead(pObj) );
+        iObjNew = Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_PI, vFanins );
+        Vec_IntWriteEntry( vReachReadCi, 3*i+2, iObjNew );
+    }
+    //Vec_IntPrint( vReachReadCi );
+
+    // duplicate flop outputs
+    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)) );
+        }
+
+/*
+    // create flops for memory objects
+    Wlc_NtkForEachObjVec( vMemFanins, p, pObj, i )
+        for ( k = 0; k < nFrames; k++ )
+            Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_FO, vFanins );
+*/
+
+    // create buffers for read ports
+    Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
+    {
+        if ( !Wlc_ObjIsRead(pObj) )
+            continue;
+        iObjNew = Wlc_ObjAlloc( pNew, WLC_OBJ_BUF, pObj->Signed, pObj->End, pObj->Beg );
+        Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), iObjNew );
+    }
+
+    // duplicate objects
+    Wlc_NtkForEachObj( p, pObj, i )
+        if ( !Wlc_ObjIsCi(pObj) && !pObj->Mark )
+            Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+
+    // create memory constraints
+    Wlc_NtkCreateMemoryConstr( pNew, p, vMemObjsClean, vReachReadCi );
+
+    // create outpus
+    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( "Memory abstraction created %d miter outputs.\n", Wlc_NtkPoNum(pNew) );
+        Wlc_NtkForEachCo( p, pObj, i )
+            if ( pObj->fIsFi && !pObj->Mark )
+                Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
+    }
+    else
+    {
+        // duplicate POs
+        Wlc_NtkForEachPo( p, pObj, i )
+            if ( !pObj->Mark )
+                Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
+        // duplicate FIs
+        Wlc_NtkForEachCo( p, pObj, i )
+            if ( !Wlc_ObjIsPo(pObj) && !pObj->Mark )
+                Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
+    }
+
+/*
+    // create new flop inputs
+    Wlc_NtkForEachObjVec( vMemFanins, p, pObj, i )
+        for ( k = 0; k < nFrames; k++ )
+            Wlc_NtkDupOneBuffer( pNew, p, pObj, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj))-(nFrames-1-k), vFanins, 1 );
+*/
+
+    // append init states
+    pNew->pInits = Wlc_PrsConvertInitValues( pNew );
+    if ( p->pSpec )
+        pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    if ( Wlc_NtkHasNameId(p) )
+        Wlc_NtkTransferNames( pNew, p );
+    Vec_IntFree( vFanins );
+    Vec_IntFree( vMemObjsAll );
+    Vec_IntFree( vMemObjsClean );
+    Vec_IntFree( vReachReadCi );
+    Wlc_NtkCleanMarks( p );
+    // derive topological order
+//printf( "Objects before = %d.\n", Wlc_NtkObjNum(pNew) );
+    pNew = Wlc_NtkDupDfs( pTemp = pNew, 0, 1 );
+    Wlc_NtkFree( pTemp );
+//printf( "Objects after = %d.\n", Wlc_NtkObjNum(pNew) );
+    return pNew;
+}
+
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index d3228de6..6e882bc1 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -832,7 +832,7 @@ void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p )
     assert( pNew->pManName  == NULL && p->pManName != NULL );
     Wlc_NtkCleanNameId( pNew );
     for ( i = 0; i < p->nObjsAlloc; i++ )
-        if ( Wlc_ObjCopy(p, i) && i < Vec_IntSize(&p->vNameIds) && Wlc_ObjNameId(p, i) )
+        if ( Wlc_ObjCopy(p, i) > 0 && i < Vec_IntSize(&p->vNameIds) && Wlc_ObjNameId(p, i) )
             Wlc_ObjSetNameId( pNew, Wlc_ObjCopy(p, i), Wlc_ObjNameId(p, i) );
     pNew->pManName = p->pManName; 
     p->pManName = NULL;
diff --git a/src/base/wlc/wlcShow.c b/src/base/wlc/wlcShow.c
index 91c6296d..f43f8baa 100644
--- a/src/base/wlc/wlcShow.c
+++ b/src/base/wlc/wlcShow.c
@@ -261,7 +261,7 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
         else
         {
             fprintf( pFile, "  Node%d [label = \"%d:%s %d\"", Wlc_ObjId(p, pNode), Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) ); 
-            fprintf( pFile, ", shape = %s", (Vec_IntSize(&p->vFfs2) > 0 || i < Wlc_NtkPiNum(p)) ? "triangle" : "box" );
+            fprintf( pFile, ", shape = %s", (Vec_IntSize(&p->vFfs2) > 0 || Wlc_ObjCiId(pNode) < Wlc_NtkPiNum(p)) ? "triangle" : "box" );
             fprintf( pFile, ", color = coral, fillcolor = coral" );
         }
         fprintf( pFile, "];\n" );
diff --git a/src/base/wln/module.make b/src/base/wln/module.make
index 30792a0c..748c104c 100644
--- a/src/base/wln/module.make
+++ b/src/base/wln/module.make
@@ -1,4 +1,5 @@
 SRC +=    src/base/wln/wln.c \
+    src/base/wln/wlnMem.c \
     src/base/wln/wlnNdr.c \
     src/base/wln/wlnNtk.c \
     src/base/wln/wlnObj.c \
diff --git a/src/base/wln/wlnMem.c b/src/base/wln/wlnMem.c
new file mode 100644
index 00000000..2a879855
--- /dev/null
+++ b/src/base/wln/wlnMem.c
@@ -0,0 +1,52 @@
+/**CFile****************************************************************
+
+  FileName    [wlnMem.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Word-level network.]
+
+  Synopsis    [Memory abstraction.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 23, 2018.]
+
+  Revision    [$Id: wlnMem.c,v 1.00 2018/09/23 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wln.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+