Experiments with memory abstraction.

8 files changed, 100 insertions, 24 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index a04e19e8..279ec6a2 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -379,7 +379,7 @@ 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 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 );
@@ -403,6 +403,7 @@ extern int            Wlc_ObjDup( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec
 extern void           Wlc_NtkFree( Wlc_Ntk_t * p );
 extern int            Wlc_NtkCreateLevels( Wlc_Ntk_t * p );
 extern int            Wlc_NtkCreateLevelsRev( Wlc_Ntk_t * p );
+extern int            Wlc_NtkRemapLevels( Wlc_Ntk_t * p, Vec_Int_t * vObjs, int nLevels );
 extern int            Wlc_NtkCountRealPis( Wlc_Ntk_t * p );
 extern void           Wlc_NtkPrintNode( Wlc_Ntk_t * p, Wlc_Obj_t * pObj );
 extern void           Wlc_NtkPrintNodeArray( Wlc_Ntk_t * p, Vec_Int_t * vArray );
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 3031f331..7e39fd32 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -317,20 +317,20 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fAllObjects  = 0;
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "cmardtovh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cbamdtovh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'c':
             fShowCones ^= 1;
             break;
-        case 'm':
+        case 'b':
             fShowMulti ^= 1;
             break;
         case 'a':
             fShowAdder ^= 1;
             break;
-        case 'r':
+        case 'm':
             fShowMem ^= 1;
             break;
         case 'd':
@@ -369,12 +369,12 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
         Wlc_NtkPrintObjects( pNtk );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%ps [-cmardtovh]\n" );
+    Abc_Print( -2, "usage: %%ps [-cbamdtovh]\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-b     : 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-r     : toggle printing memories [default = %s]\n",              fShowMem?   "yes": "no" );
+    Abc_Print( -2, "\t-m     : toggle printing memories [default = %s]\n",              fShowMem?   "yes": "no" );
     Abc_Print( -2, "\t-d     : toggle printing distrubition [default = %s]\n",          fDistrib?   "yes": "no" );
     Abc_Print( -2, "\t-t     : toggle printing stats for LHS and RHS [default = %s]\n", fTwoSides?  "yes": "no" );
     Abc_Print( -2, "\t-o     : toggle printing all objects [default = %s]\n",           fAllObjects?"yes": "no" );
@@ -1443,7 +1443,7 @@ int Abc_CommandShow( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( fMemory )
     {
-        Vec_Int_t * vTemp = Wlc_NtkCollectMemory( pNtk );
+        Vec_Int_t * vTemp = Wlc_NtkCollectMemory( pNtk, 1 );
         Wlc_NtkShow( pNtk, vTemp );
         Vec_IntFree( vTemp );
     }
@@ -1811,7 +1811,7 @@ usage:
 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);
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@@ -1844,6 +1844,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     //Wln_ReadNdrTest();
     //pNtk = Wlc_NtkMemAbstractTest( pNtk );
     //Wlc_AbcUpdateNtk( pAbc, pNtk );
+    //Wln_NtkFromWlcTest( pNtk );
     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 fd844b62..b61ddad0 100644
--- a/src/base/wlc/wlcMem.c
+++ b/src/base/wlc/wlcMem.c
@@ -184,7 +184,35 @@ Vec_Int_t * Wlc_NtkCollectMemSizes( Wlc_Ntk_t * p )
     }
     return vMemSizes;
 }
-Vec_Int_t * Wlc_NtkCollectMemory( Wlc_Ntk_t * p )
+// remove PIs without fanout, non-driven object and their fanouts
+int Wlc_ObjCheckIsEmpty_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
+{
+    int k, iFanin;
+    if ( Wlc_ObjType(pObj) == 0 )
+        return 1;
+    if ( Wlc_ObjIsPi(pObj) )
+        return Vec_IntEntry(&p->vRefs, Wlc_ObjId(p, pObj)) == 0;
+    else if ( Wlc_ObjIsCi(pObj) )
+        return 0;
+    Wlc_ObjForEachFanin( pObj, iFanin, k )
+        if ( !Wlc_ObjCheckIsEmpty_rec(p, Wlc_NtkObj(p, iFanin)) )
+            return 0;
+    return 1;
+}
+Vec_Int_t * Wlc_NtkCleanObjects( Wlc_Ntk_t * p, Vec_Int_t * vObjs )
+{
+    Wlc_Obj_t * pObj; int i;
+    Vec_Int_t * vMemObjs = Vec_IntAlloc( 10 );
+    Wlc_NtkSetRefs( p );
+    Wlc_NtkForEachObjVec( vObjs, p, pObj, i )
+    {
+        //printf( "Considering %d (%s)\n", Wlc_ObjId(p, pObj), Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
+        if ( !Wlc_ObjCheckIsEmpty_rec(p, pObj) )
+            Vec_IntPush( vMemObjs, Wlc_ObjId(p, pObj) );
+    }
+    return vMemObjs;
+}
+Vec_Int_t * Wlc_NtkCollectMemory( Wlc_Ntk_t * p, int fClean )
 {
     Wlc_Obj_t * pObj; int i;
     Vec_Int_t * vMemSizes = Wlc_NtkCollectMemSizes( p );
@@ -197,13 +225,21 @@ Vec_Int_t * Wlc_NtkCollectMemory( Wlc_Ntk_t * p )
             Vec_IntPush( vMemObjs, i );
     }
     Vec_IntFree( vMemSizes );
+    Vec_IntSort( vMemObjs, 0 );
+    //Wlc_NtkPrintNodeArray( p, vMemObjs ); 
+    if ( fClean )
+    {
+        Vec_Int_t * vTemp;
+        vMemObjs = Wlc_NtkCleanObjects( p, vTemp = vMemObjs );
+        Vec_IntFree( vTemp );
+    }
     return vMemObjs;
 }
 void Wlc_NtkPrintMemory( Wlc_Ntk_t * p )
 {
     Vec_Int_t * vMemory;
-    vMemory = Wlc_NtkCollectMemory( p );
-    Vec_IntSort( vMemory, 0 );
+    vMemory = Wlc_NtkCollectMemory( p, 1 );
+    printf( "Memory subsystem is composed of the following objects:\n" );
     Wlc_NtkPrintNodeArray( p, vMemory );
     Vec_IntFree( vMemory );
 }
@@ -917,7 +953,7 @@ Wlc_Ntk_t * Wlc_NtkMemAbstractTest( Wlc_Ntk_t * p )
 {
     int iFirstMemPi, iFirstCi, iFirstMemCi, nDcBits;
     Vec_Int_t * vRefine;
-    Vec_Int_t * vMemObjs    = Wlc_NtkCollectMemory( p );
+    Vec_Int_t * vMemObjs    = Wlc_NtkCollectMemory( p, 0 );
     Vec_Int_t * vMemFanins  = Wlc_NtkCollectMemFanins( p, vMemObjs );
 
     Vec_Wec_t * vRefines    = Vec_WecAlloc( 100 );
@@ -956,7 +992,7 @@ int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fDumpAbs, int fPdrVerbo
     Vec_Int_t * vMemObjs, * vMemFanins, * vFirstTotal, * vRefine; 
     int RetValue = -1, iFirstMemPi, iFirstCi, iFirstMemCi, nDcBits, nIters;
 
-    vMemObjs    = Wlc_NtkCollectMemory( p );
+    vMemObjs    = Wlc_NtkCollectMemory( p, 0 );
     vMemFanins  = Wlc_NtkCollectMemFanins( p, vMemObjs );
     pNewFull    = Wlc_NtkAbstractMemory( p, vMemObjs, vMemFanins, &iFirstMemPi, &iFirstCi, &iFirstMemCi, NULL, NULL );
     nDcBits     = Wlc_CountDcs( pNewFull->pInits );
diff --git a/src/base/wlc/wlcNdr.c b/src/base/wlc/wlcNdr.c
index 43827b53..9ced4e18 100644
--- a/src/base/wlc/wlcNdr.c
+++ b/src/base/wlc/wlcNdr.c
@@ -155,7 +155,7 @@ int Ndr_TypeWlc2Ndr( int Type )
     if ( Type == WLC_OBJ_ARI_SQUARE )     return ABC_OPER_ARI_SQUARE;   // 52: integer square
     if ( Type == WLC_OBJ_ARI_ADDSUB )     return ABC_OPER_ARI_ADDSUB;   // 56: adder-subtractor
     if ( Type == WLC_OBJ_ARI_MULTI )      return ABC_OPER_ARI_SMUL;     // 45: signed multiplier
-    if ( Type == WLC_OBJ_FO )             return ABC_OPER_DFF;          // 03: flop
+    if ( Type == WLC_OBJ_FO )             return ABC_OPER_DFFRSE;       // 03: flop
     if ( Type == WLC_OBJ_FF )             return ABC_OPER_DFFRSE;       // 05: flop
     if ( Type == WLC_OBJ_READ )           return ABC_OPER_RAMR;         // 54: read port
     if ( Type == WLC_OBJ_WRITE )          return ABC_OPER_RAMW;         // 55: write port
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index b7743ba5..d3228de6 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -378,9 +378,40 @@ int Wlc_NtkCreateLevels( Wlc_Ntk_t * p )
     LeveMax = Vec_IntFindMax( &p->vLevels );
     Wlc_NtkForEachFf2( p, pObj, i )
         Vec_IntWriteEntry( &p->vLevels, Wlc_ObjId(p, pObj), LeveMax+1 );
-    Wlc_NtkPrintObjects( p ); 
+    //Wlc_NtkPrintObjects( p ); 
     return LeveMax+1;
 }
+int Wlc_NtkRemapLevels( Wlc_Ntk_t * p, Vec_Int_t * vObjs, int nLevels )
+{
+    int i, k, iFanin, iObj, Entry, Level = 0, Res = nLevels;
+    Vec_Int_t * vMap  = Vec_IntStart( nLevels+1 );
+    Vec_Int_t * vUsed = Vec_IntStart( nLevels+1 );
+    // mark used levels
+    Vec_IntWriteEntry( vUsed, nLevels, 1 );
+    Vec_IntForEachEntry( vObjs, iObj, i )
+    {
+        Vec_IntWriteEntry( vUsed, Wlc_ObjLevelId(p, iObj), 1 );
+        Wlc_ObjForEachFanin( Wlc_NtkObj(p, iObj), iFanin, k ) if ( iFanin )
+            Vec_IntWriteEntry( vUsed, Wlc_ObjLevelId(p, iFanin), 1 );
+    }
+    // create level map
+    Vec_IntForEachEntry( vUsed, Entry, i )
+        if ( Entry )
+            Vec_IntWriteEntry( vMap, i, Level++ );
+    //printf( "Total used levels %d -> %d\n", nLevels, Level );
+    // remap levels
+    Vec_IntForEachEntry( &p->vLevels, Level, i )
+    {
+        if ( Vec_IntEntry(vUsed, Level) )
+            Vec_IntWriteEntry( &p->vLevels, i, Vec_IntEntry(vMap, Level) );
+        else
+            Vec_IntWriteEntry( &p->vLevels, i, -1 );
+    }
+    Res = Vec_IntEntry( vMap, nLevels );
+    Vec_IntFree( vUsed );
+    Vec_IntFree( vMap );
+    return Res;
+}
 
 /**Function*************************************************************
 
@@ -674,17 +705,17 @@ void Wlc_NtkPrintNode( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
     printf( "%6d%s = ", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s" : " " );
     if ( pObj->Type == WLC_OBJ_PI )
     {
-        printf( "PI\n" );
+        printf( "            PI                   :    %-12s\n", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
         return;
     }
     if ( pObj->Type == WLC_OBJ_FO )
     {
-        printf( "FO\n" );
+        printf( "            FO                   :    %-12s = %-12s\n", Wlc_ObjName(p, Wlc_ObjId(p, pObj)), Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFo2Fi(p, pObj))) );
         return;
     }
     if ( pObj->Type != WLC_OBJ_CONST && Wlc_ObjFaninNum(pObj) == 0 )
     {
-        printf( "Unknown object without fanins\n" );
+        printf( "Unknown object without fanins    :    %-12s\n", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
         return;
     }
     if ( pObj->Type != WLC_OBJ_CONST )
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index 9c40e71e..0eca5c26 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -1029,9 +1029,9 @@ startword:
                         Wlc_ObjSetCi( p->pNtk, pObj );
                 Vec_IntClear( &p->pNtk->vFfs );
                 // convert init values into binary string
-                //Vec_IntPrint( &p->pNtk->vInits );
+                //Vec_IntPrint( p->pNtk->vInits );
                 p->pNtk->pInits = Wlc_PrsConvertInitValues( p->pNtk );
-                //printf( "%s", p->pNtk->pInits );
+                //printf( "%s\n", p->pNtk->pInits );
             }
             if ( p->vPoPairs )
             {
diff --git a/src/base/wlc/wlcShow.c b/src/base/wlc/wlcShow.c
index 50da3e5b..91c6296d 100644
--- a/src/base/wlc/wlcShow.c
+++ b/src/base/wlc/wlcShow.c
@@ -67,6 +67,8 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
 
     // compute levels
     LevelMax = 1 + Wlc_NtkCreateLevels( p );
+    if ( vBold )
+        LevelMax = Wlc_NtkRemapLevels( p, vBold, LevelMax );
 
 //    Wlc_NtkForEachObj( p, pNode, i )
 //        printf( "Obj=%d Lev=%d\n", i, Wlc_ObjLevel(p, pNode) );
@@ -131,7 +133,7 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
     fprintf( pFile, "          label=\"" );
     fprintf( pFile, "%s", "WLC structure generated by ABC" );
     fprintf( pFile, "\\n" );
-    fprintf( pFile, "Benchmark \\\"%s\\\". ", p->pName );
+    fprintf( pFile, "Benchmark \\\"%s\\\" from file \\\"%s\\\". ", p->pName, p->pSpec ? Extra_FileNameWithoutPath(p->pSpec) : "unknown" );
 //    fprintf( pFile, "Time was %s. ",  Extra_TimeStamp() );
     fprintf( pFile, "\"\n" );
     fprintf( pFile, "         ];\n" );
@@ -359,7 +361,12 @@ void Wlc_NtkShow( Wlc_Ntk_t * p, Vec_Int_t * vBold )
     extern void Abc_ShowFile( char * FileNameDot );
     FILE * pFile;
     char FileNameDot[200];
-    sprintf( FileNameDot, "%s", Extra_FileNameGenericAppend(p->pName, ".dot") );
+    char * pName = Extra_FileDesignName(p->pName);
+    char * pSpec = p->pSpec ? Extra_FileDesignName(p->pSpec) : "unknown";
+    sprintf( FileNameDot, "%s_%s.dot", pName, pSpec );
+    ABC_FREE( pName );
+    if ( strcmp(pSpec, "unknown") )
+        ABC_FREE( pSpec );
     // check that the file can be opened
     if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
     {
diff --git a/src/base/wlc/wlcWriteVer.c b/src/base/wlc/wlcWriteVer.c
index 30f10e14..90d49ade 100644
--- a/src/base/wlc/wlcWriteVer.c
+++ b/src/base/wlc/wlcWriteVer.c
@@ -578,7 +578,7 @@ void Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName, int fAddCos, int fNoFlops )
         fprintf( stdout, "Wlc_WriteVer(): Cannot open the output file \"%s\".\n", pFileName );
         return;
     }
-    fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", p->pName, Extra_TimeStamp() );
+    fprintf( pFile, "// Benchmark \"%s\" from file \"%s\" written by ABC on %s\n", p->pName, p->pSpec ? p->pSpec : "unknown", Extra_TimeStamp() );
     fprintf( pFile, "\n" );
     Wlc_WriteTables( pFile, p );
     if ( fAddCos )