Adding visualization of word-level networks Wlc_Ntk_t.

7 files changed, 617 insertions, 11 deletions

diff --git a/src/base/wlc/module.make b/src/base/wlc/module.make
index 5a95a63f..ae7899ec 100644
--- a/src/base/wlc/module.make
+++ b/src/base/wlc/module.make
@@ -7,6 +7,7 @@ SRC +=    src/base/wlc/wlcAbs.c \
     src/base/wlc/wlcReadSmt.c \
     src/base/wlc/wlcReadVer.c \
     src/base/wlc/wlcSim.c \
+    src/base/wlc/wlcShow.c \
     src/base/wlc/wlcStdin.c \
     src/base/wlc/wlcWin.c \
     src/base/wlc/wlcWriteVer.c 
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 6f64b47a..e4a818e5 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -157,6 +157,7 @@ struct Wlc_Ntk_t_
     Vec_Int_t              vTravIds;           // trav IDs of the objects
     Vec_Int_t              vCopies;            // object first bits
     Vec_Int_t              vBits;              // object mapping into AIG nodes
+    Vec_Int_t              vLevels;            // object levels
 };
 
 static inline int          Wlc_NtkObjNum( Wlc_Ntk_t * p )                           { return p->iObj - 1;                                                      }
@@ -206,6 +207,8 @@ static inline int          Wlc_ObjSign( Wlc_Obj_t * p )
 static inline int *        Wlc_ObjConstValue( Wlc_Obj_t * p )                       { assert(p->Type == WLC_OBJ_CONST);      return Wlc_ObjFanins(p);          }
 static inline int          Wlc_ObjTableId( Wlc_Obj_t * p )                          { assert(p->Type == WLC_OBJ_TABLE);      return p->Fanins[1];              }
 static inline word *       Wlc_ObjTable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )          { return (word *)Vec_PtrEntry( p->vTables, Wlc_ObjTableId(pObj) );         }
+static inline int          Wlc_ObjLevelId( Wlc_Ntk_t * p, int iObj )                { return Vec_IntEntry( &p->vLevels, iObj );                                }
+static inline int          Wlc_ObjLevel( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )          { return Wlc_ObjLevelId( p, Wlc_ObjId(p, pObj) );                          }
 
 static inline void         Wlc_NtkCleanCopy( Wlc_Ntk_t * p )                        { Vec_IntFill( &p->vCopies, p->nObjsAlloc, 0 );                            }
 static inline int          Wlc_NtkHasCopy( Wlc_Ntk_t * p )                          { return Vec_IntSize( &p->vCopies ) > 0;                                   }
@@ -230,6 +233,8 @@ static inline Wlc_Obj_t *  Wlc_ObjFoToFi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
 
 #define Wlc_NtkForEachObj( p, pObj, i )                                             \
     for ( i = 1; (i < Wlc_NtkObjNumMax(p)) && (((pObj) = Wlc_NtkObj(p, i)), 1); i++ )
+#define Wlc_NtkForEachObjReverse( p, pObj, i )                                      \
+    for ( i = Wlc_NtkObjNumMax(p) - 1; (i > 0) && (((pObj) = Wlc_NtkObj(p, i)), 1); i-- )
 #define Wlc_NtkForEachObjVec( vVec, p, pObj, i )                                    \
     for ( i = 0; (i < Vec_IntSize(vVec)) && (((pObj) = Wlc_NtkObj(p, Vec_IntEntry(vVec, i))), 1); i++ )
 #define Wlc_NtkForEachPi( p, pPi, i )                                               \
@@ -266,6 +271,7 @@ extern Gia_Man_t *    Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int i
 /*=== wlcCom.c ========================================================*/
 extern void           Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk );
 /*=== wlcNtk.c ========================================================*/
+extern char *         Wlc_ObjTypeName( Wlc_Obj_t * p );
 extern Wlc_Ntk_t *    Wlc_NtkAlloc( char * pName, int nObjsAlloc );
 extern int            Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg );
 extern int            Wlc_ObjCreate( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg, Vec_Int_t * vFanins );
@@ -275,12 +281,16 @@ 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 void           Wlc_NtkFree( Wlc_Ntk_t * p );
+extern int            Wlc_NtkCreateLevels( Wlc_Ntk_t * p );
+extern int            Wlc_NtkCreateLevelsRev( 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 );
 extern void           Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type );
 extern void           Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose );
-extern Wlc_Ntk_t *    Wlc_NtkDupDfs( Wlc_Ntk_t * p );
+extern Wlc_Ntk_t *    Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked );
 extern void           Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p );
+extern void           Wlc_NtkCleanMarks( Wlc_Ntk_t * p );
+extern void           Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iPo );
 extern Wlc_Ntk_t *    Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p );
 /*=== wlcReadSmt.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit, int fOldParser, int fPrintTree );
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index 73ff7328..368652d6 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -173,7 +173,7 @@ Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit )
     if ( vNodes != vNodesInit )
         Vec_IntFree( vNodes );
     // reconstruct topological order
-    pNew = Wlc_NtkDupDfs( p );
+    pNew = Wlc_NtkDupDfs( p, 0 );
     Wlc_NtkTransferNames( pNew, p );
     return pNew;
 }
@@ -278,7 +278,7 @@ Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * p, Vec_Int_t * vPairsInit )
     if ( vPairs != vPairsInit )
         Vec_IntFree( vPairs );
     // reconstruct topological order
-    pNew = Wlc_NtkDupDfs( p );
+    pNew = Wlc_NtkDupDfs( p, 0 );
     Wlc_NtkTransferNames( pNew, p );
     return pNew;
 }
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 2828fea3..316d2883 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -31,8 +31,10 @@ ABC_NAMESPACE_IMPL_START
 static int  Abc_CommandReadWlc  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandPs       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandCone     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandBlast    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandProfile  ( 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 );
@@ -68,8 +70,10 @@ void Wlc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Word level", "%read",       Abc_CommandReadWlc,   0 );
     Cmd_CommandAdd( pAbc, "Word level", "%write",      Abc_CommandWriteWlc,  0 );
     Cmd_CommandAdd( pAbc, "Word level", "%ps",         Abc_CommandPs,        0 );
+    Cmd_CommandAdd( pAbc, "Word level", "%cone",       Abc_CommandCone,      0 );
     Cmd_CommandAdd( pAbc, "Word level", "%blast",      Abc_CommandBlast,     0 );
     Cmd_CommandAdd( pAbc, "Word level", "%profile",    Abc_CommandProfile,   0 );
+    Cmd_CommandAdd( pAbc, "Word level", "%show",       Abc_CommandShow,      0 );
     Cmd_CommandAdd( pAbc, "Word level", "%test",       Abc_CommandTest,      0 );
 
     Cmd_CommandAdd( pAbc, "Word level", "inv_ps",      Abc_CommandInvPs,     0 );
@@ -343,6 +347,70 @@ usage:
   SeeAlso     []
 
 ******************************************************************************/
+int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    int c, iOutput = -1, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Ovh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'O':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            iOutput = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( iOutput < 0 )
+                goto usage;
+            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;
+    }
+    if ( iOutput < 0 || iOutput >= Wlc_NtkPoNum(pNtk) )
+    {
+        Abc_Print( 1, "Abc_CommandCone(): Illegal output index (%d) (should be 0 <= num < %d).\n", iOutput, Wlc_NtkPoNum(pNtk) );
+        return 0;
+    }
+    printf( "Extracting output %d.\n", iOutput );
+    Wlc_NtkMarkCone( pNtk, iOutput );
+    pNtk = Wlc_NtkDupDfs( pNtk, 1 );
+    Wlc_AbcUpdateNtk( pAbc, pNtk );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%cone [-O num] [-vh]\n" );
+    Abc_Print( -2, "\t         extracts cone of the given word-level output\n" );
+    Abc_Print( -2, "\t-O num : zero-based index of the word-level output to extract [default = %d]\n", iOutput );
+    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 )
 {
     Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
@@ -481,6 +549,54 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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;
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    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" );
+#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" );
+#endif
+    Abc_Print( -2, "\t-h    : print the command usage\n");
+    return 1;
+}
+
 /**Function********************************************************************
 
   Synopsis    []
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index a0799ba0..fa0074d3 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -88,6 +88,8 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = {
     NULL                   // 54: unused
 };
 
+char * Wlc_ObjTypeName( Wlc_Obj_t * p ) { return Wlc_Names[p->Type]; }
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -224,6 +226,7 @@ void Wlc_NtkFree( Wlc_Ntk_t * p )
     ABC_FREE( p->vValues.pArray );
     ABC_FREE( p->vCopies.pArray );
     ABC_FREE( p->vBits.pArray );
+    ABC_FREE( p->vLevels.pArray );
     ABC_FREE( p->pInits );
     ABC_FREE( p->pObjs );
     ABC_FREE( p->pName );
@@ -246,6 +249,81 @@ int Wlc_NtkMemUsage( Wlc_Ntk_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Assigns object levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Wlc_NtkCreateLevels( Wlc_Ntk_t * p )
+{
+    Wlc_Obj_t * pObj; 
+    int i, k, iFanin, Level, LevelMax = 0;
+    Vec_IntFill( &p->vLevels, Wlc_NtkObjNumMax(p), 0 );
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        Level = 0;
+        Wlc_ObjForEachFanin( pObj, iFanin, k )
+            Level = Abc_MaxInt( Level, Wlc_ObjLevelId(p, iFanin) + 1 );
+        Vec_IntWriteEntry( &p->vLevels, i, Level );
+        LevelMax = Abc_MaxInt( LevelMax, Level );
+    }
+    return LevelMax;
+}
+int Wlc_NtkCreateLevelsRev( Wlc_Ntk_t * p )
+{
+    Wlc_Obj_t * pObj; 
+    int i, k, iFanin, Level, LevelMax = 0;
+    Vec_IntFill( &p->vLevels, Wlc_NtkObjNumMax(p), 0 );
+    Wlc_NtkForEachObjReverse( p, pObj, i )
+    {
+        if ( Wlc_ObjIsCi(pObj) )
+            continue;
+        Level = Wlc_ObjLevel(p, pObj) + 1;
+        Wlc_ObjForEachFanin( pObj, iFanin, k )
+            Vec_IntUpdateEntry( &p->vLevels, iFanin, Level );
+        LevelMax = Abc_MaxInt( LevelMax, Level );
+    }
+    // reverse the values
+    Wlc_NtkForEachObj( p, pObj, i )
+        Vec_IntWriteEntry( &p->vLevels, i, LevelMax - Wlc_ObjLevelId(p, i) );
+    Wlc_NtkForEachCi( p, pObj, i )
+        Vec_IntWriteEntry( &p->vLevels, Wlc_ObjId(p, pObj), 0 );
+    return LevelMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects statistics for each side of the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_NtkCollectStats( Wlc_Ntk_t * p, int nObjs[2][WLC_OBJ_NUMBER] )
+{
+    Wlc_Obj_t * pObj;
+    int n, i;
+    if ( Wlc_NtkPoNum(p) != 2 )
+        return;
+    for ( n = 0; n < 2; n++ )
+    {
+        Wlc_NtkMarkCone( p, n );
+        Wlc_NtkForEachObj( p, pObj, i )
+            if ( pObj->Mark )
+                nObjs[n][pObj->Type]++;
+    }
+    Wlc_NtkCleanMarks( p );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Prints distribution of operator types.]
 
   Description []
@@ -300,11 +378,13 @@ void Wlc_NtkPrintDistribSortOne( Vec_Ptr_t * vTypes, Vec_Ptr_t * vOccurs, int Ty
 }
 void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
 {
+    int nObjs[2][WLC_OBJ_NUMBER] = {{0}}; // counter of objects of each type
     Wlc_Obj_t * pObj, * pObjRange = NULL; int nCountRange = 0;
     Vec_Ptr_t * vTypes, * vOccurs;
     Vec_Int_t * vAnds = Vec_IntStart( WLC_OBJ_NUMBER );
     word Sign;
     int i, k, s, s0, s1;
+    Wlc_NtkCollectStats( p, nObjs );
     // allocate statistics arrays
     vTypes  = Vec_PtrStart( WLC_OBJ_NUMBER );
     vOccurs = Vec_PtrStart( WLC_OBJ_NUMBER );
@@ -435,28 +515,40 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
         else if ( pObj->Type == WLC_OBJ_ARI_SQUARE )    
             Vec_IntAddToEntry( vAnds, WLC_OBJ_ARI_SQUARE,   5 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) * Wlc_ObjRange(Wlc_ObjFanin1(p, pObj))  );
     }
-    if ( nCountRange )
+    if ( nCountRange && Vec_IntSize(&p->vNameIds) > 0 )
     {
         printf( "Warning: %d objects of the design have non-zero-based ranges.\n", nCountRange );
         printf( "In particular, object %6d with name \"%s\" has range %d=[%d:%d]\n", Wlc_ObjId(p, pObjRange), 
             Abc_NamStr(p->pManName, Wlc_ObjNameId(p, Wlc_ObjId(p, pObjRange))), Wlc_ObjRange(pObjRange), pObjRange->End, pObjRange->Beg );
     }
     // print by occurrence
-    printf( "ID  :  name  occurrence    and2 (occurrence)<output_range>=<input_range>.<input_range> ...\n" );
+    printf( "ID  :  name  occurrence%s    and2 (occurrence)<output_range>=<input_range>.<input_range> ...\n", Wlc_NtkPoNum(p) == 2 ? "     Left Share Right":"" );
     for ( i = 0; i < WLC_OBJ_NUMBER; i++ )
     {
         Vec_Wrd_t * vType  = (Vec_Wrd_t *)Vec_PtrEntry( vTypes, i );
         Vec_Wrd_t * vOccur = (Vec_Wrd_t *)Vec_PtrEntry( vOccurs, i );
         if ( p->nObjs[i] == 0 )
             continue;
-        printf( "%2d  :  %-8s  %6d%8d ", i, Wlc_Names[i], p->nObjs[i], Vec_IntEntry(vAnds, i) );
+        printf( "%2d  :  %-8s  %6d", i, Wlc_Names[i], p->nObjs[i] );
+        if ( Wlc_NtkPoNum(p) == 2 )
+        {
+            printf( "   " );
+            printf( "%6d", nObjs[0][i] );
+            printf( "%6d", nObjs[0][i]+nObjs[1][i]-p->nObjs[i] );
+            printf( "%6d", nObjs[1][i] );
+        }
+        printf( "%8d ", Vec_IntEntry(vAnds, i) );
         // sort by occurence
         Wlc_NtkPrintDistribSortOne( vTypes, vOccurs, i );
         Vec_WrdForEachEntry( vType, Sign, k )
         {
             Wlc_NtkPrintDistribFromSign( Sign, &s, &s0, &s1 );
             if ( ((k % 6) == 5 && s1) || ((k % 8) == 7 && !s1) )
+            {
                 printf( "\n                                " );
+                if ( Wlc_NtkPoNum(p) == 2 )
+                    printf( "                     " );
+            }
             printf( "(%d)", (int)Vec_WrdEntry( vOccur, k ) );
             printf( "%s%d",      Abc_LitIsCompl(s)?"-":"",  Abc_Lit2Var(s) );
             if ( s0 )
@@ -623,7 +715,7 @@ void Wlc_NtkDupDfs_rec( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * v
         Wlc_NtkDupDfs_rec( pNew, p, iFanin, vFanins );
     Wlc_ObjDup( pNew, p, iObj, vFanins );
 }
-Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p )
+Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked )
 {
     Wlc_Ntk_t * pNew;
     Wlc_Obj_t * pObj;
@@ -634,11 +726,14 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p )
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
     pNew->fSmtLib = p->fSmtLib;
     Wlc_NtkForEachCi( p, pObj, i )
-        Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+        if ( !fMarked || pObj->Mark )
+            Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
     Wlc_NtkForEachCo( p, pObj, i )
-        Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+        if ( !fMarked || pObj->Mark )
+            Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
     Wlc_NtkForEachCo( p, pObj, i )
-        Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
+        if ( !fMarked || pObj->Mark )
+            Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
     if ( p->vInits )
     pNew->vInits = Vec_IntDup( p->vInits );
     if ( p->pInits )
@@ -668,6 +763,59 @@ void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Select the cone of the given output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_NtkCleanMarks( Wlc_Ntk_t * p )
+{
+    Wlc_Obj_t * pObj;
+    int i;
+    Wlc_NtkForEachObj( p, pObj, i )
+        pObj->Mark = 0;
+}
+void Wlc_NtkMarkCone_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFlops )
+{
+    int i, iFanin;
+    if ( pObj->Mark )
+        return;
+    pObj->Mark = 1;
+    if ( Wlc_ObjIsCi(pObj) )
+    {
+        if ( !Wlc_ObjIsPi(pObj) )
+            Vec_IntPush( vFlops, Wlc_ObjCiId(pObj) );
+        return;
+    }
+    Wlc_ObjForEachFanin( pObj, iFanin, i )
+        Wlc_NtkMarkCone_rec( p, Wlc_NtkObj(p, iFanin), vFlops );
+}
+void Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iPo )
+{
+    Vec_Int_t * vFlops;
+    Wlc_Obj_t * pObj;
+    int i, CiId, CoId;
+    Wlc_NtkCleanMarks( p );
+    Wlc_NtkForEachPi( p, pObj, i )
+        pObj->Mark = 1;
+    vFlops = Vec_IntAlloc( 100 );
+    Wlc_NtkForEachPo( p, pObj, i )
+        if ( i == iPo )
+            Wlc_NtkMarkCone_rec( p, pObj, vFlops );
+    Vec_IntForEachEntry( vFlops, CiId, i )
+    {
+        CoId = Wlc_NtkPoNum(p) + CiId - Wlc_NtkPiNum(p);
+        Wlc_NtkMarkCone_rec( p, Wlc_NtkCo(p, CoId), vFlops );
+    }
+    Vec_IntFree( vFlops );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates the network by copying each node.]
 
   Description []
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index fa3efacd..2959f4a1 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -1265,7 +1265,7 @@ Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr )
     if ( !Wlc_PrsDerive( p ) )
         goto finish;
     // derive topological order
-    pNtk = Wlc_NtkDupDfs( p->pNtk );
+    pNtk = Wlc_NtkDupDfs( p->pNtk, 0 );
     Wlc_NtkTransferNames( pNtk, p->pNtk );
     pNtk->pSpec = Abc_UtilStrsav( pFileName );
 finish:
diff --git a/src/base/wlc/wlcShow.c b/src/base/wlc/wlcShow.c
new file mode 100644
index 00000000..dd25c7a3
--- /dev/null
+++ b/src/base/wlc/wlcShow.c
@@ -0,0 +1,331 @@
+/**CFile****************************************************************
+
+  FileName    [wlcShow.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of word-level Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 22, 2014.]
+
+  Revision    [$Id: wlcShow.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wlc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the graph structure of WLC for DOT.]
+
+  Description [Useful for graph visualization using tools such as GraphViz: 
+  http://www.graphviz.org/]
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
+{
+    FILE * pFile;
+    Wlc_Obj_t * pNode;
+    int LevelMax, Prev, Level, i;
+
+    if ( Wlc_NtkObjNum(p) > 500 )
+    {
+        fprintf( stdout, "Cannot visualize WLC with more than %d nodes.\n", 500 );
+        return;
+    }
+    if ( (pFile = fopen( pFileName, "w" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName );
+        return;
+    }
+
+    // mark the nodes
+    if ( vBold )
+        Wlc_NtkForEachObjVec( vBold, p, pNode, i )
+            pNode->Mark = 1;
+
+    // compute levels
+    LevelMax = 1 + Wlc_NtkCreateLevelsRev( p );
+
+    // write the DOT header
+    fprintf( pFile, "# %s\n",  "WLC structure generated by ABC" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "digraph WLC {\n" );
+    fprintf( pFile, "size = \"7.5,10\";\n" );
+//  fprintf( pFile, "ranksep = 0.5;\n" );
+//  fprintf( pFile, "nodesep = 0.5;\n" );
+    fprintf( pFile, "center = true;\n" );
+//  fprintf( pFile, "orientation = landscape;\n" );
+//  fprintf( pFile, "edge [fontsize = 10];\n" );
+//  fprintf( pFile, "edge [dir = none];\n" );
+    fprintf( pFile, "edge [dir = back];\n" );
+    fprintf( pFile, "\n" );
+
+    // labels on the left of the picture
+    fprintf( pFile, "{\n" );
+    fprintf( pFile, "  node [shape = plaintext];\n" );
+    fprintf( pFile, "  edge [style = invis];\n" );
+    fprintf( pFile, "  LevelTitle1 [label=\"\"];\n" );
+    fprintf( pFile, "  LevelTitle2 [label=\"\"];\n" );
+    // generate node names with labels
+    for ( Level = LevelMax; Level >= 0; Level-- )
+    {
+        // the visible node name
+        fprintf( pFile, "  Level%d", Level );
+        fprintf( pFile, " [label = " );
+        // label name
+        fprintf( pFile, "\"" );
+        fprintf( pFile, "\"" );
+        fprintf( pFile, "];\n" );
+    }
+
+    // genetate the sequence of visible/invisible nodes to mark levels
+    fprintf( pFile, "  LevelTitle1 ->  LevelTitle2 ->" );
+    for ( Level = LevelMax; Level >= 0; Level-- )
+    {
+        // the visible node name
+        fprintf( pFile, "  Level%d",  Level );
+        // the connector
+        if ( Level != 0 )
+            fprintf( pFile, " ->" );
+        else
+            fprintf( pFile, ";" );
+    }
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+
+    // generate title box on top
+    fprintf( pFile, "{\n" );
+    fprintf( pFile, "  rank = same;\n" );
+    fprintf( pFile, "  LevelTitle1;\n" );
+    fprintf( pFile, "  title1 [shape=plaintext,\n" );
+    fprintf( pFile, "          fontsize=20,\n" );
+    fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
+    fprintf( pFile, "          label=\"" );
+    fprintf( pFile, "%s", "WLC structure generated by ABC" );
+    fprintf( pFile, "\\n" );
+    fprintf( pFile, "Benchmark \\\"%s\\\". ", p->pName );
+//    fprintf( pFile, "Time was %s. ",  Extra_TimeStamp() );
+    fprintf( pFile, "\"\n" );
+    fprintf( pFile, "         ];\n" );
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+
+    // generate statistics box
+    fprintf( pFile, "{\n" );
+    fprintf( pFile, "  rank = same;\n" );
+    fprintf( pFile, "  LevelTitle2;\n" );
+    fprintf( pFile, "  title2 [shape=plaintext,\n" );
+    fprintf( pFile, "          fontsize=18,\n" );
+    fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
+    fprintf( pFile, "          label=\"" );
+    fprintf( pFile, "The word-level network contains %d nodes and spans %d levels.", Wlc_NtkObjNum(p)-Wlc_NtkPiNum(p)-Wlc_NtkPoNum(p)-Wlc_NtkFfNum(p), LevelMax-1 );
+    fprintf( pFile, "\\n" );
+    fprintf( pFile, "\"\n" );
+    fprintf( pFile, "         ];\n" );
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+
+    // generate the COs
+    fprintf( pFile, "{\n" );
+    fprintf( pFile, "  rank = same;\n" );
+    // the labeling node of this level
+    fprintf( pFile, "  Level%d;\n",  LevelMax );
+    // generate the CO nodes
+    Wlc_NtkForEachCo( p, pNode, i )
+    {
+        fprintf( pFile, "  NodePo%d [label = \"%s %d\"", Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) ); 
+        fprintf( pFile, ", shape = %s", "invtriangle" );
+        fprintf( pFile, ", color = coral, fillcolor = coral" );
+        fprintf( pFile, "];\n" );
+    }
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+
+    // generate nodes of each rank
+    for ( Level = LevelMax - 1; Level > 0; Level-- )
+    {
+        fprintf( pFile, "{\n" );
+        fprintf( pFile, "  rank = same;\n" );
+        // the labeling node of this level
+        fprintf( pFile, "  Level%d;\n",  Level );
+        Wlc_NtkForEachObj( p, pNode, i )
+        {
+            if ( (int)Wlc_ObjLevel(p, pNode) != Level )
+                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 );
+                fprintf( pFile, "\"" ); 
+            }
+            else if ( pNode->Type == WLC_OBJ_BUF || pNode->Type == WLC_OBJ_MUX )
+                fprintf( pFile, "  Node%d [label = \"%d\"", i, Wlc_ObjRange(pNode) ); 
+            else if ( pNode->Type >= WLC_OBJ_LOGIC_NOT && pNode->Type <= WLC_OBJ_COMP_MOREEQU )
+                fprintf( pFile, "  Node%d [label = \"%s\"", i, Wlc_ObjTypeName(pNode) ); 
+            else
+                fprintf( pFile, "  Node%d [label = \"%s %d\"", i, Wlc_ObjTypeName(pNode), Wlc_ObjRange(pNode) ); 
+
+            if ( pNode->Type == WLC_OBJ_ARI_MULTI )
+                fprintf( pFile, ", shape = doublecircle" );
+            else if ( pNode->Type >= WLC_OBJ_COMP_EQU && pNode->Type <= WLC_OBJ_COMP_MOREEQU )
+                fprintf( pFile, ", shape = diamond" );
+            else if ( pNode->Type == WLC_OBJ_BIT_SELECT || pNode->Type == WLC_OBJ_BIT_CONCAT )
+                fprintf( pFile, ", shape = box" );
+            else if ( pNode->Type == WLC_OBJ_BUF || pNode->Type == WLC_OBJ_BIT_ZEROPAD || pNode->Type == WLC_OBJ_BIT_SIGNEXT )
+                fprintf( pFile, ", shape = triangle" );
+            else if ( pNode->Type == WLC_OBJ_MUX )
+                fprintf( pFile, ", shape = trapezium" );
+            else
+                fprintf( pFile, ", shape = ellipse" );
+
+            if ( vBold ? pNode->Mark : ((pNode->Type >= WLC_OBJ_ARI_ADD && pNode->Type <= WLC_OBJ_ARI_SQUARE) || pNode->Type == WLC_OBJ_BIT_NOT) )
+                fprintf( pFile, ", style = filled" );
+            fprintf( pFile, "];\n" );
+        }
+        fprintf( pFile, "}" );
+        fprintf( pFile, "\n" );
+        fprintf( pFile, "\n" );
+    }
+
+    // generate the CI nodes
+    fprintf( pFile, "{\n" );
+    fprintf( pFile, "  rank = same;\n" );
+    // the labeling node of this level
+    fprintf( pFile, "  Level%d;\n",  0 );
+    // generate the CI nodes
+    Wlc_NtkForEachCi( p, pNode, i )
+    {
+        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", "triangle" );
+        fprintf( pFile, ", color = coral, fillcolor = coral" );
+        fprintf( pFile, "];\n" );
+    }
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+
+    // generate invisible edges from the square down
+    fprintf( pFile, "title1 -> title2 [style = invis];\n" );
+    Wlc_NtkForEachCo( p, pNode, i )
+        fprintf( pFile, "title2 -> NodePo%d [style = invis];\n", Wlc_ObjId(p, pNode) );
+    // generate invisible edges among the COs
+    Prev = -1;
+    Wlc_NtkForEachCo( p, pNode, i )
+    {
+        if ( i > 0 )
+            fprintf( pFile, "NodePo%d -> NodePo%d [style = invis];\n", Prev, Wlc_ObjId(p, pNode) );
+        Prev = Wlc_ObjId(p, pNode);
+    }
+    // generate invisible edges among the CIs
+    Prev = -1;
+    Wlc_NtkForEachCi( p, pNode, i )
+    {
+        if ( i > 0 )
+            fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Wlc_ObjId(p, pNode) );
+        Prev = Wlc_ObjId(p, pNode);
+    }
+
+    // generate edges
+    Wlc_NtkForEachObj( p, pNode, i )
+    {
+        int k, iFanin;
+        if ( Wlc_ObjIsCi(pNode) )
+            continue;
+        if ( Wlc_ObjIsCo(pNode) )
+        {
+            // generate the edge from this node to the next
+            fprintf( pFile, "NodePo%d",  i );
+            fprintf( pFile, " -> " );
+            fprintf( pFile, "Node%d",  i );
+            fprintf( pFile, " [" );
+            fprintf( pFile, "style = %s", pNode->Signed? "dotted" : "bold" );
+            fprintf( pFile, "]" );
+            fprintf( pFile, ";\n" );
+        }
+        // generate the edge from this node to the next
+        Wlc_ObjForEachFanin( pNode, iFanin, k )
+        {
+            fprintf( pFile, "Node%d",  i );
+            fprintf( pFile, " -> " );
+            fprintf( pFile, "Node%d",  iFanin );
+            fprintf( pFile, " [" );
+            fprintf( pFile, "style = %s", Wlc_NtkObj(p, iFanin)->Signed? "dotted" : "bold" );
+            fprintf( pFile, "]" );
+            fprintf( pFile, ";\n" );
+        }
+    }
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+
+    // unmark nodes
+    if ( vBold )
+        Wlc_NtkCleanMarks( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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") );
+    // check that the file can be opened
+    if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
+        return;
+    }
+    fclose( pFile );
+    // generate the file
+    Wlc_NtkDumpDot( p, FileNameDot, vBold );
+    // visualize the file 
+    Abc_ShowFile( FileNameDot );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+