Experiments with memory abstraction.

12 files changed, 327 insertions, 25 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 9189927b..d06292d5 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1135,6 +1135,10 @@ SOURCE=.\src\base\wln\wlnRetime.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\wln\wlnWlc.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\wln\wlnWriteVer.c
 # End Source File
 # End Group
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 )
diff --git a/src/base/wln/module.make b/src/base/wln/module.make
index 6689baf0..30792a0c 100644
--- a/src/base/wln/module.make
+++ b/src/base/wln/module.make
@@ -3,4 +3,5 @@ SRC +=    src/base/wln/wln.c \
     src/base/wln/wlnNtk.c \
     src/base/wln/wlnObj.c \
     src/base/wln/wlnRetime.c \
+    src/base/wln/wlnWlc.c \
     src/base/wln/wlnWriteVer.c 
diff --git a/src/base/wln/wlnWlc.c b/src/base/wln/wlnWlc.c
new file mode 100644
index 00000000..6de55de4
--- /dev/null
+++ b/src/base/wln/wlnWlc.c
@@ -0,0 +1,221 @@
+/**CFile****************************************************************
+
+  FileName    [wlnWlc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Word-level network.]
+
+  Synopsis    [Network transformation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 23, 2018.]
+
+  Revision    [$Id: wlnWlc.c,v 1.00 2018/09/23 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wln.h"
+#include "base/wlc/wlc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern int Ndr_TypeWlc2Ndr( int Type );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Wln_ConstFromBits( unsigned * pBits, int nBits )
+{
+    char * pBuffer = ABC_ALLOC( char, nBits+100 ); int i, Len;
+    sprintf( pBuffer, "%d\'b", nBits );
+    Len = strlen(pBuffer);
+    for ( i = nBits-1; i >= 0; i-- )
+        pBuffer[Len++] = '0' + Abc_InfoHasBit(pBits, i);
+    pBuffer[Len] = 0;
+    return pBuffer;
+}
+char * Wln_ConstFromStr( char * pBits, int nBits )
+{
+    char * pBuffer = ABC_ALLOC( char, nBits+100 ); int i, Len;
+    sprintf( pBuffer, "%d\'b", nBits );
+    Len = strlen(pBuffer);
+    for ( i = 0; i < nBits; i++ )
+        pBuffer[Len++] = pBits[i];
+    pBuffer[Len] = 0;
+    return pBuffer;
+}
+int Wln_TrasformNameId( Wln_Ntk_t * pNew, Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
+{
+    return Abc_NamStrFindOrAdd( pNew->pManName, Wlc_ObjName(p, Wlc_ObjId(p, pObj)), NULL );
+}
+Wln_Ntk_t * Wln_NtkFromWlc( Wlc_Ntk_t * p )
+{
+    Wlc_Obj_t * pObj; 
+    char Buffer[1000];
+    int i, j, n, Type, iFanin, iOutId, iBit = 0;
+    Vec_Int_t * vFanins = Vec_IntAlloc( 10 );
+    Vec_Int_t * vInits = Vec_IntAlloc( Wlc_NtkFfNum(p) );
+    Wln_Ntk_t * pNew = Wln_NtkAlloc( p->pName, Wlc_NtkObjNum(p)+Wlc_NtkCoNum(p)+Wlc_NtkFfNum(p) );
+    pNew->pManName = Abc_NamStart( Abc_NamObjNumMax(p->pManName), 10 );
+    if ( p->pSpec ) pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    pNew->fSmtLib = p->fSmtLib;
+    Wlc_NtkCleanCopy( p );
+    Wln_NtkCleanNameId( pNew );
+    // add primary inputs
+    Wlc_NtkForEachPi( p, pObj, i ) 
+    {
+        iOutId = Wln_ObjAlloc( pNew, ABC_OPER_CI, pObj->Signed, pObj->End, pObj->Beg );
+        Wln_ObjSetNameId( pNew, iOutId, Wln_TrasformNameId(pNew, p, pObj) );
+        Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), iOutId );
+    }
+    // create initial state of the flops
+    Wlc_NtkForEachCi( p, pObj, i ) 
+    {
+        assert( i == Wlc_ObjCiId(pObj) );
+        if ( pObj->Type == WLC_OBJ_PI )
+            continue;
+        for ( j = 0; j < Wlc_ObjRange(pObj); j++ )
+            if ( p->pInits[iBit+j] == 'x' )
+                break;
+        // print flop init state
+        if ( 1 )
+        {
+            printf( "Flop %3d init state: %d\'b", i-Wlc_NtkPiNum(p), Wlc_ObjRange(pObj) );
+            if ( j == Wlc_ObjRange(pObj) )
+            {
+                int Count = 0;
+                for ( n = 0; n < Wlc_ObjRange(pObj); n++ )
+                    Count += p->pInits[iBit+n] == '0';
+                if ( Count == Wlc_ObjRange(pObj) )
+                    printf( "0" );
+                else
+                    for ( n = 0; n < Wlc_ObjRange(pObj); n++ )
+                        printf( "%c", p->pInits[iBit+n] );
+            }
+            else
+            {
+                int Count = 0;
+                for ( n = 0; n < Wlc_ObjRange(pObj); n++ )
+                    Count += p->pInits[iBit+n] == 'x';
+                printf( "x" );
+                if ( Count != Wlc_ObjRange(pObj) )
+                    printf( " (range %d)", Wlc_ObjRange(pObj) );
+            }
+            printf( "\n" );
+        }
+        Type = j == Wlc_ObjRange(pObj) ? ABC_OPER_CONST : ABC_OPER_CI; 
+        iOutId = Wln_ObjAlloc( pNew, Type, pObj->Signed, pObj->End, pObj->Beg );
+        if ( j == Wlc_ObjRange(pObj) ) // constant
+        {
+            char * pString = Wln_ConstFromStr(p->pInits + iBit, Wlc_ObjRange(pObj));
+            Wln_ObjSetConst( pNew, iOutId, Abc_NamStrFindOrAdd(pNew->pManName, pString, NULL) );
+            ABC_FREE( pString );
+        }
+        sprintf( Buffer, "ff_init_%d", Vec_IntSize(vInits) );
+        Wln_ObjSetNameId( pNew, iOutId, Abc_NamStrFindOrAdd(pNew->pManName, Buffer, NULL) );
+        Vec_IntPush( vInits, iOutId );
+        iBit += Wlc_ObjRange(pObj);
+    }
+    assert( p->pInits == NULL || iBit == (int)strlen(p->pInits) );
+    // add flop outputs
+    Wlc_NtkForEachCi( p, pObj, i ) 
+    {
+        assert( i == Wlc_ObjCiId(pObj) );
+        if ( pObj->Type == WLC_OBJ_PI )
+            continue;
+        iOutId = Wln_ObjAlloc( pNew, ABC_OPER_DFFRSE, pObj->Signed, pObj->End, pObj->Beg );
+        Wln_ObjSetNameId( pNew, iOutId, Wln_TrasformNameId(pNew, p, pObj) );
+        Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), iOutId );
+    }
+    // add internal nodes 
+    Wlc_NtkForEachObj( p, pObj, i ) 
+    {
+        if ( Wlc_ObjIsCi(pObj) || pObj->Type == 0 )
+            continue;
+        iOutId = Wln_ObjAlloc( pNew, Ndr_TypeWlc2Ndr(pObj->Type), pObj->Signed, pObj->End, pObj->Beg );
+        Vec_IntClear( vFanins );
+        Wlc_ObjForEachFanin( pObj, iFanin, n )
+            Vec_IntPush( vFanins, Wlc_ObjCopy(p, iFanin) );
+        Wln_ObjAddFanins( pNew, iOutId, vFanins );
+        if ( pObj->Type == WLC_OBJ_BIT_SELECT )
+            Wln_ObjSetSlice( pNew, iOutId, Hash_Int2ManInsert(pNew->pRanges, pObj->End, pObj->Beg, 0) );
+        else if ( pObj->Type == WLC_OBJ_CONST )
+        {
+            char * pString = Wln_ConstFromBits(Wlc_ObjConstValue(pObj), Wlc_ObjRange(pObj));
+            Wln_ObjSetConst( pNew, iOutId, Abc_NamStrFindOrAdd(pNew->pManName, pString, NULL) );
+            ABC_FREE( pString );
+        }
+//        else if ( Type == ABC_OPER_BIT_MUX && Vec_IntSize(vFanins) == 3 )
+//            ABC_SWAP( int, Wln_ObjFanins(p, iObj)[1], Wln_ObjFanins(p, iObj)[2] );
+        Wln_ObjSetNameId( pNew, iOutId, Wln_TrasformNameId(pNew, p, pObj) );
+        Wlc_ObjSetCopy( p, i, iOutId );
+    }
+    Wlc_NtkForEachPo( p, pObj, i ) 
+    {
+        iOutId = Wln_ObjAlloc( pNew, ABC_OPER_CO, pObj->Signed, pObj->End, pObj->Beg );
+        Wln_ObjAddFanin( pNew, iOutId, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)) );
+        //Wln_ObjSetNameId( pNew, iOutId, Wln_TrasformNameId(pNew, p, pObj) );
+    }
+    assert( Vec_IntSize(vInits) == Wlc_NtkCoNum(p) - Wlc_NtkPoNum(p) );
+    Wlc_NtkForEachCo( p, pObj, i ) 
+    {
+        if ( i < Wlc_NtkPoNum(p) )
+            continue;
+        //char * pInNames[8] = {"d", "clk", "reset", "set", "enable", "async", "sre", "init"};
+        Vec_IntClear( vFanins );
+        Vec_IntPush( vFanins, Wlc_ObjCopy(p, Wlc_ObjFaninId0(pObj)) );
+        for ( n = 0; n < 6; n++ )
+            Vec_IntPush( vFanins, 0 );
+        Vec_IntPush( vFanins, Vec_IntEntry(vInits, i-Wlc_NtkPoNum(p)) );
+        Wln_ObjAddFanins( pNew, Vec_IntEntry(&pNew->vFfs, i-Wlc_NtkPoNum(p)), vFanins );
+    }
+    Vec_IntFree( vFanins );
+    Vec_IntFree( vInits );
+    return pNew;
+}
+void Wln_NtkFromWlcTest( Wlc_Ntk_t * p )
+{
+    Wln_Ntk_t * pNew = Wln_NtkFromWlc( p );
+    Wln_WriteVer( pNew, "test_wlc2wln.v" );
+    Wln_NtkFree( pNew );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/wln/wlnWriteVer.c b/src/base/wln/wlnWriteVer.c
index 1c37e311..e0849bf4 100644
--- a/src/base/wln/wlnWriteVer.c
+++ b/src/base/wln/wlnWriteVer.c
@@ -475,7 +475,7 @@ void Wln_WriteVer( Wln_Ntk_t * p, char * pFileName )
         fprintf( stdout, "Wln_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" );
     Wln_WriteTables( pFile, p );
 //    if ( fAddCos )