Adding visualization of word-level networks Wlc_Ntk_t.

7 files changed, 331 insertions, 115 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index e4a818e5..b898078f 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -221,7 +221,8 @@ static inline int          Wlc_NtkHasNameId( Wlc_Ntk_t * p )
 static inline void         Wlc_ObjSetNameId( Wlc_Ntk_t * p, int iObj, int i )       { Vec_IntWriteEntry( &p->vNameIds, iObj, i );                              }
 static inline int          Wlc_ObjNameId( Wlc_Ntk_t * p, int iObj )                 { return Vec_IntEntry( &p->vNameIds, iObj );                               }
 
-static inline Wlc_Obj_t *  Wlc_ObjFoToFi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )        { assert( pObj->Type == WLC_OBJ_FO ); return Wlc_NtkCo(p, Wlc_NtkCoNum(p) - Wlc_NtkCiNum(p) + Wlc_ObjCiId(pObj)); } 
+static inline Wlc_Obj_t *  Wlc_ObjFo2Fi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )          { assert( pObj->Type == WLC_OBJ_FO ); return Wlc_NtkCo(p, Wlc_NtkPoNum(p) + Wlc_ObjCiId(pObj) - Wlc_NtkPiNum(p)); } 
+static inline Wlc_Obj_t *  Wlc_ObjCo2PoFo( Wlc_Ntk_t * p, int iCoId )               { return iCoId < Wlc_NtkPoNum(p) ? Wlc_NtkPo(p, iCoId) : Wlc_NtkCi(p, Wlc_NtkPiNum(p) + iCoId - Wlc_NtkPoNum(p)); } 
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
@@ -283,15 +284,19 @@ extern void           Wlc_ObjAddFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int
 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_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 );
 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, int fMarked );
+extern void           Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fTwoSides, int fVerbose );
 extern void           Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p );
+extern char *         Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq );
+extern Wlc_Ntk_t *    Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq );
 extern void           Wlc_NtkCleanMarks( Wlc_Ntk_t * p );
-extern void           Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iPo );
+extern void           Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int fSeq );
+extern void           Wlc_NtkProfileCones( Wlc_Ntk_t * p );
 extern Wlc_Ntk_t *    Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p );
+extern void           Wlc_NtkShortNames( Wlc_Ntk_t * p );
 /*=== wlcReadSmt.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit, int fOldParser, int fPrintTree );
 extern Wlc_Ntk_t *    Wlc_ReadSmt( char * pFileName, int fOldParser, int fPrintTree );
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index 368652d6..ce6b8de9 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -173,8 +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, 0 );
-    Wlc_NtkTransferNames( pNew, p );
+    pNew = Wlc_NtkDupDfs( p, 0, 1 );
     return pNew;
 }
 
@@ -278,8 +277,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, 0 );
-    Wlc_NtkTransferNames( pNew, p );
+    pNew = Wlc_NtkDupDfs( p, 0, 1 );
     return pNew;
 }
 
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 316d2883..9f36ad56 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -28,21 +28,22 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-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 );
-static int  Abc_CommandInvPrint ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int  Abc_CommandInvCheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int  Abc_CommandInvGet   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int  Abc_CommandInvPut   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int  Abc_CommandInvMin   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_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_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandShow       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandTest       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int  Abc_CommandInvPs      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandInvPrint   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandInvCheck   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandInvGet     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandInvPut     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandInvMin     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc )                       { return (Wlc_Ntk_t *)pAbc->pAbcWlc;                      }
 static inline void        Wlc_AbcFreeNtk( Abc_Frame_t * pAbc )                      { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc));  }
@@ -67,21 +68,22 @@ static inline Vec_Int_t * Wlc_AbcGetInv( Abc_Frame_t * pAbc )
 ******************************************************************************/
 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 );
-    Cmd_CommandAdd( pAbc, "Word level", "inv_print",   Abc_CommandInvPrint,  0 );
-    Cmd_CommandAdd( pAbc, "Word level", "inv_check",   Abc_CommandInvCheck,  0 );
-    Cmd_CommandAdd( pAbc, "Word level", "inv_get",     Abc_CommandInvGet,    0 );
-    Cmd_CommandAdd( pAbc, "Word level", "inv_put",     Abc_CommandInvPut,    0 );
-    Cmd_CommandAdd( pAbc, "Word level", "inv_min",     Abc_CommandInvMin,    0 );
+    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", "%short_names", Abc_CommandShortNames, 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 );
+    Cmd_CommandAdd( pAbc, "Word level", "inv_print",    Abc_CommandInvPrint,   0 );
+    Cmd_CommandAdd( pAbc, "Word level", "inv_check",    Abc_CommandInvCheck,   0 );
+    Cmd_CommandAdd( pAbc, "Word level", "inv_get",      Abc_CommandInvGet,     0 );
+    Cmd_CommandAdd( pAbc, "Word level", "inv_put",      Abc_CommandInvPut,     0 );
+    Cmd_CommandAdd( pAbc, "Word level", "inv_min",      Abc_CommandInvMin,     0 );
 }
 
 /**Function********************************************************************
@@ -287,15 +289,20 @@ usage:
 int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    int fShowCones   = 0;
     int fShowMulti   = 0;
     int fShowAdder   = 0;
     int fDistrib     = 0;
+    int fTwoSides    = 0;
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "madvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cmadtvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'c':
+            fShowCones ^= 1;
+            break;
         case 'm':
             fShowMulti ^= 1;
             break;
@@ -305,6 +312,9 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             fDistrib ^= 1;
             break;
+        case 't':
+            fTwoSides ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -319,19 +329,23 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Abc_CommandPs(): There is no current design.\n" );
         return 0;
     }
-    Wlc_NtkPrintStats( pNtk, fDistrib, fVerbose );
+    Wlc_NtkPrintStats( pNtk, fDistrib, fTwoSides, fVerbose );
+    if ( fShowCones )
+        Wlc_NtkProfileCones( pNtk ); 
     if ( fShowMulti )
         Wlc_NtkPrintNodes( pNtk, WLC_OBJ_ARI_MULTI );
     if ( fShowAdder )
         Wlc_NtkPrintNodes( pNtk, WLC_OBJ_ARI_ADD );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%ps [-madvh]\n" );
+    Abc_Print( -2, "usage: %%ps [-cmadtvh]\n" );
     Abc_Print( -2, "\t         prints statistics\n" );
-    Abc_Print( -2, "\t-m     : toggle printing multipliers [default = %s]\n",         fShowMulti? "yes": "no" );
-    Abc_Print( -2, "\t-a     : toggle printing adders [default = %s]\n",              fShowAdder? "yes": "no" );
-    Abc_Print( -2, "\t-d     : toggle printing distrubition [default = %s]\n",        fDistrib? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-c     : toggle printing cones [default = %s]\n",                 fShowCones? "yes": "no" );
+    Abc_Print( -2, "\t-m     : toggle printing multipliers [default = %s]\n",           fShowMulti? "yes": "no" );
+    Abc_Print( -2, "\t-a     : toggle printing adders [default = %s]\n",                fShowAdder? "yes": "no" );
+    Abc_Print( -2, "\t-d     : toggle printing distrubition [default = %s]\n",          fDistrib? "yes": "no" );
+    Abc_Print( -2, "\t-t     : toggle printing stats for LHS and RHS [default = %s]\n", fTwoSides? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",   fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -350,9 +364,10 @@ usage:
 int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
-    int c, iOutput = -1, fVerbose  = 0;
+    int c, iOutput = -1, fSeq = 0, fVerbose  = 0;
+    char * pName;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Ovh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Osvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -367,6 +382,9 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( iOutput < 0 )
                 goto usage;
             break;
+        case 's':
+            fSeq ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -381,20 +399,24 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
         return 0;
     }
-    if ( iOutput < 0 || iOutput >= Wlc_NtkPoNum(pNtk) )
+    if ( iOutput < 0 || iOutput >= Wlc_NtkCoNum(pNtk) )
     {
-        Abc_Print( 1, "Abc_CommandCone(): Illegal output index (%d) (should be 0 <= num < %d).\n", iOutput, Wlc_NtkPoNum(pNtk) );
+        Abc_Print( 1, "Abc_CommandCone(): Illegal output index (%d) (should be 0 <= num < %d).\n", iOutput, Wlc_NtkCoNum(pNtk) );
         return 0;
     }
-    printf( "Extracting output %d.\n", iOutput );
-    Wlc_NtkMarkCone( pNtk, iOutput );
-    pNtk = Wlc_NtkDupDfs( pNtk, 1 );
+    printf( "Extracting output %d as a %s word-level network.\n", iOutput, fSeq ? "sequential" : "combinational" );
+    pName = Wlc_NtkNewName( pNtk, iOutput, fSeq );
+    Wlc_NtkMarkCone( pNtk, iOutput, fSeq );
+    pNtk = Wlc_NtkDupDfs( pNtk, 1, fSeq );
+    ABC_FREE( pNtk->pName );
+    pNtk->pName = Abc_UtilStrsav( pName );
     Wlc_AbcUpdateNtk( pAbc, pNtk );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%cone [-O num] [-vh]\n" );
+    Abc_Print( -2, "usage: %%cone [-O num] [-svh]\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-s     : toggle performing extracting sequential cones [default = %s]\n", fSeq? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -549,6 +571,50 @@ usage:
     return 1;
 }
 
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" );
+        return 0;
+    }
+    Wlc_NtkShortNames( pNtk );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%short_names [-vh]\n" );
+    Abc_Print( -2, "\t         derives short names for all objects of the network\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index fa0074d3..822c2eb5 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -314,13 +314,23 @@ void Wlc_NtkCollectStats( Wlc_Ntk_t * p, int nObjs[2][WLC_OBJ_NUMBER] )
         return;
     for ( n = 0; n < 2; n++ )
     {
-        Wlc_NtkMarkCone( p, n );
+        Wlc_NtkMarkCone( p, n, 1 );
         Wlc_NtkForEachObj( p, pObj, i )
             if ( pObj->Mark )
                 nObjs[n][pObj->Type]++;
     }
     Wlc_NtkCleanMarks( p );
 }
+int Wlc_NtkCountRealPis( Wlc_Ntk_t * p )
+{
+    Wlc_Obj_t * pObj;
+    int i, Count = 0;
+    Wlc_NtkMarkCone( p, -1, 1 );
+    Wlc_NtkForEachPi( p, pObj, i )
+        Count += pObj->Mark;
+    Wlc_NtkCleanMarks( p );
+    return Count;
+}
 
 /**Function*************************************************************
 
@@ -376,7 +386,7 @@ void Wlc_NtkPrintDistribSortOne( Vec_Ptr_t * vTypes, Vec_Ptr_t * vOccurs, int Ty
     Vec_WrdReverseOrder( vType );
     Vec_WrdReverseOrder( vOccur );
 }
-void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
+void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fTwoSides, int fVerbose )
 {
     int nObjs[2][WLC_OBJ_NUMBER] = {{0}}; // counter of objects of each type
     Wlc_Obj_t * pObj, * pObjRange = NULL; int nCountRange = 0;
@@ -384,7 +394,10 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
     Vec_Int_t * vAnds = Vec_IntStart( WLC_OBJ_NUMBER );
     word Sign;
     int i, k, s, s0, s1;
-    Wlc_NtkCollectStats( p, nObjs );
+    if ( Wlc_NtkPoNum(p) != 2 )
+        fTwoSides = 0;
+    if ( fTwoSides )
+        Wlc_NtkCollectStats( p, nObjs );
     // allocate statistics arrays
     vTypes  = Vec_PtrStart( WLC_OBJ_NUMBER );
     vOccurs = Vec_PtrStart( WLC_OBJ_NUMBER );
@@ -489,11 +502,11 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
         else if ( pObj->Type == WLC_OBJ_REDUCT_XOR )   
             Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_XOR,   3 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 3 );
         else if ( pObj->Type == WLC_OBJ_REDUCT_NAND )   
-            Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NAND,       Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 );
+            Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NAND,      Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 );
         else if ( pObj->Type == WLC_OBJ_REDUCT_NOR )    
-            Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NOR,        Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 );
+            Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NOR,       Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 );
         else if ( pObj->Type == WLC_OBJ_REDUCT_NXOR )   
-            Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NXOR,   3 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 3 );
+            Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NXOR,  3 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 3 );
         else if ( pObj->Type == WLC_OBJ_ARI_ADD )       
             Vec_IntAddToEntry( vAnds, WLC_OBJ_ARI_ADD,      9 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) );
         else if ( pObj->Type == WLC_OBJ_ARI_SUB )       
@@ -522,7 +535,7 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
             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%s    and2 (occurrence)<output_range>=<input_range>.<input_range> ...\n", Wlc_NtkPoNum(p) == 2 ? "     Left Share Right":"" );
+    printf( "ID  :  name  occurrence%s    and2 (occurrence)<output_range>=<input_range>.<input_range> ...\n", fTwoSides ? "     Left Share Right":"" );
     for ( i = 0; i < WLC_OBJ_NUMBER; i++ )
     {
         Vec_Wrd_t * vType  = (Vec_Wrd_t *)Vec_PtrEntry( vTypes, i );
@@ -530,11 +543,12 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
         if ( p->nObjs[i] == 0 )
             continue;
         printf( "%2d  :  %-8s  %6d", i, Wlc_Names[i], p->nObjs[i] );
-        if ( Wlc_NtkPoNum(p) == 2 )
+        if ( fTwoSides )
         {
+            int nTotal = i == WLC_OBJ_PI ? Wlc_NtkCountRealPis(p) : p->nObjs[i];
             printf( "   " );
             printf( "%6d", nObjs[0][i] );
-            printf( "%6d", nObjs[0][i]+nObjs[1][i]-p->nObjs[i] );
+            printf( "%6d", nObjs[0][i]+nObjs[1][i]-nTotal );
             printf( "%6d", nObjs[1][i] );
         }
         printf( "%8d ", Vec_IntEntry(vAnds, i) );
@@ -546,7 +560,7 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
             if ( ((k % 6) == 5 && s1) || ((k % 8) == 7 && !s1) )
             {
                 printf( "\n                                " );
-                if ( Wlc_NtkPoNum(p) == 2 )
+                if ( fTwoSides )
                     printf( "                     " );
             }
             printf( "(%d)", (int)Vec_WrdEntry( vOccur, k ) );
@@ -627,11 +641,11 @@ void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type )
         Wlc_NtkPrintNode( p, pObj );
     }
 }
-void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose )
+void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fTwoSides, int fVerbose )
 {
     int i;
     printf( "%-20s : ",        p->pName );
-    printf( "PI = %4d  ",      Wlc_NtkPiNum(p) );
+    printf( "PI = %4d  ",      Wlc_NtkCountRealPis(p) ); //Wlc_NtkPiNum(p) );
     printf( "PO = %4d  ",      Wlc_NtkPoNum(p) );
     printf( "FF = %4d  ",      Wlc_NtkFfNum(p) );
     printf( "Obj = %6d  ",     Wlc_NtkObjNum(p) );
@@ -639,7 +653,7 @@ void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose )
     printf( "\n" );
     if ( fDistrib )
     {
-        Wlc_NtkPrintDistrib( p, fVerbose );
+        Wlc_NtkPrintDistrib( p, fTwoSides, fVerbose );
         return;
     }
     if ( !fVerbose )
@@ -658,6 +672,41 @@ void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p )
+{
+    int i;
+    assert( !Wlc_NtkHasCopy(pNew)   && Wlc_NtkHasCopy(p)   );
+    assert( !Wlc_NtkHasNameId(pNew) && Wlc_NtkHasNameId(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) )
+            Wlc_ObjSetNameId( pNew, Wlc_ObjCopy(p, i), Wlc_ObjNameId(p, i) );
+    pNew->pManName = p->pManName; 
+    p->pManName = NULL;
+    Vec_IntErase( &p->vNameIds );
+    // transfer table
+    pNew->pMemTable = p->pMemTable;  p->pMemTable = NULL;
+    pNew->vTables = p->vTables;      p->vTables = NULL;
+}
+char * Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq )
+{
+    static char pBuffer[1000];
+    sprintf( pBuffer, "%s_o%d_%s", p->pName, iCoId, fSeq ? "seq": "comb" );
+    return pBuffer;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates the network in a topological order.]
 
   Description []
@@ -715,51 +764,43 @@ 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, int fMarked )
+Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq )
 {
     Wlc_Ntk_t * pNew;
     Wlc_Obj_t * pObj;
     Vec_Int_t * vFanins;
     int i;
-    Wlc_NtkCleanCopy( p );
     vFanins = Vec_IntAlloc( 100 );
+    Wlc_NtkCleanCopy( p );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
     pNew->fSmtLib = p->fSmtLib;
     Wlc_NtkForEachCi( p, pObj, i )
         if ( !fMarked || pObj->Mark )
+        {
+            unsigned Type = pObj->Type;
+            if ( !fSeq ) pObj->Type = WLC_OBJ_PI;
             Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+            pObj->Type = Type;
+        }
     Wlc_NtkForEachCo( p, pObj, i )
         if ( !fMarked || pObj->Mark )
             Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
     Wlc_NtkForEachCo( p, pObj, i )
         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 )
-    pNew->pInits = Abc_UtilStrsav( p->pInits );
+            Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), fSeq ? pObj->fIsFi : 0 );
     Vec_IntFree( vFanins );
+    if ( !fMarked )
+    {
+        if ( p->vInits )
+            pNew->vInits = Vec_IntDup( p->vInits );
+        if ( p->pInits )
+            pNew->pInits = Abc_UtilStrsav( p->pInits );
+    }
     if ( p->pSpec )
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Wlc_NtkTransferNames( pNew, p );
     return pNew;
 }
-void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p )
-{
-    int i;
-    assert( !Wlc_NtkHasCopy(pNew)   && Wlc_NtkHasCopy(p)   );
-    assert( !Wlc_NtkHasNameId(pNew) && Wlc_NtkHasNameId(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) )
-            Wlc_ObjSetNameId( pNew, Wlc_ObjCopy(p, i), Wlc_ObjNameId(p, i) );
-    pNew->pManName = p->pManName; 
-    p->pManName = NULL;
-    Vec_IntErase( &p->vNameIds );
-    // transfer table
-    pNew->pMemTable = p->pMemTable;  p->pMemTable = NULL;
-    pNew->vTables = p->vTables;      p->vTables = NULL;
-}
 
 /**Function*************************************************************
 
@@ -779,6 +820,30 @@ void Wlc_NtkCleanMarks( Wlc_Ntk_t * p )
     Wlc_NtkForEachObj( p, pObj, i )
         pObj->Mark = 0;
 }
+int Wlc_NtkCountMarked( Wlc_Ntk_t * p, int * pnPis, int * pnFos, int * pnAdders, int * pnMults )
+{
+    Wlc_Obj_t * pObj;
+    int i, nNodes = 0;
+    *pnPis = *pnFos = *pnAdders = *pnMults = 0;
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        if ( !pObj->Mark )
+            continue;
+        if ( Wlc_ObjIsPi(pObj) )
+            (*pnPis)++;
+        else if ( Wlc_ObjIsCi(pObj) )
+            (*pnFos)++;
+        else if ( pObj->Mark )
+        {
+            nNodes++;
+            if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB )
+                (*pnAdders)++;
+            else if ( pObj->Type == WLC_OBJ_ARI_MULTI )
+                (*pnMults)++;
+        }
+    }
+    return nNodes;
+}
 void Wlc_NtkMarkCone_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFlops )
 {
     int i, iFanin;
@@ -794,18 +859,19 @@ void Wlc_NtkMarkCone_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFlops )
     Wlc_ObjForEachFanin( pObj, iFanin, i )
         Wlc_NtkMarkCone_rec( p, Wlc_NtkObj(p, iFanin), vFlops );
 }
-void Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iPo )
+void Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int fSeq )
 {
     Vec_Int_t * vFlops;
     Wlc_Obj_t * pObj;
     int i, CiId, CoId;
     Wlc_NtkCleanMarks( p );
-    Wlc_NtkForEachPi( p, pObj, i )
-        pObj->Mark = 1;
+//    Wlc_NtkForEachPi( p, pObj, i )
+//        pObj->Mark = 1;
     vFlops = Vec_IntAlloc( 100 );
-    Wlc_NtkForEachPo( p, pObj, i )
-        if ( i == iPo )
+    Wlc_NtkForEachCo( p, pObj, i )
+        if ( iCoId == -1 || i == iCoId )
             Wlc_NtkMarkCone_rec( p, pObj, vFlops );
+    if ( fSeq )
     Vec_IntForEachEntry( vFlops, CiId, i )
     {
         CoId = Wlc_NtkPoNum(p) + CiId - Wlc_NtkPiNum(p);
@@ -813,6 +879,24 @@ void Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iPo )
     }
     Vec_IntFree( vFlops );
 }
+void Wlc_NtkProfileCones( Wlc_Ntk_t * p )
+{
+    Wlc_Obj_t * pObj; 
+    int i, nPis, nFos, nNodes, nAdders, nMults;
+    Wlc_NtkForEachCo( p, pObj, i )
+    {
+        Wlc_NtkMarkCone( p, i, 0 );
+        nNodes = Wlc_NtkCountMarked( p, &nPis, &nFos, &nAdders, &nMults );
+        printf( "Cone %5d : ", i );
+        printf( "PI = %4d  ", nPis );
+        printf( "FO = %4d  ", nFos );
+        printf( "Node = %6d  ", nNodes );
+        printf( "Add/Sub = %4d  ", nAdders );
+        printf( "Mult = %4d  ", nMults );
+        printf( "\n" );
+    }
+    Wlc_NtkCleanMarks( p );
+}
 
 /**Function*************************************************************
 
@@ -871,6 +955,64 @@ Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Creates short names for all objects.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_NtkShortNames( Wlc_Ntk_t * p )
+{
+    Wlc_Obj_t * pObj;
+    char pBuffer[100];
+    int nDigits, NameId, fFound, i;
+    int nFlops = Wlc_NtkCoNum(p) - Wlc_NtkPoNum(p);
+    nDigits = Abc_Base10Log( nFlops );
+    Wlc_NtkForEachCo( p, pObj, i )
+    {
+        if ( Wlc_ObjIsPo(pObj) )
+            continue;
+        sprintf( pBuffer, "%s%0*d", "fi", nDigits, i - Wlc_NtkPoNum(p) );
+        NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound );
+        Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId );
+    }
+    Wlc_NtkForEachCi( p, pObj, i )
+    {
+        if ( Wlc_ObjIsPi(pObj) )
+            continue;
+        sprintf( pBuffer, "%s%0*d", "fo", nDigits, i - Wlc_NtkPiNum(p) );
+        NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound );
+        Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId );
+    }
+    nDigits = Abc_Base10Log( Wlc_NtkPoNum(p) );
+    Wlc_NtkForEachPo( p, pObj, i )
+    {
+        sprintf( pBuffer, "%s%0*d", "po", nDigits, i );
+        NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound );
+        Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId );
+    }
+    nDigits = Abc_Base10Log( Wlc_NtkPiNum(p) );
+    Wlc_NtkForEachPi( p, pObj, i )
+    {
+        sprintf( pBuffer, "%s%0*d", "pi", nDigits, i );
+        NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound );
+        Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId );
+    }
+    nDigits = Abc_Base10Log( Wlc_NtkObjNum(p) );
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        if ( Wlc_ObjIsCi(pObj) || Wlc_ObjIsCo(pObj) )
+            continue;
+        sprintf( pBuffer, "%s%0*d", "n", nDigits, i );
+        NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound );
+        Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId );
+    }
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index 2959f4a1..e4a65ecf 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -28,7 +28,7 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 
 // Word-level Verilog file parser
-#define WLV_PRS_MAX_LINE   1000
+#define WLV_PRS_MAX_LINE   10000
 
 typedef struct Wlc_Prs_t_  Wlc_Prs_t;
 struct Wlc_Prs_t_ 
@@ -1265,8 +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, 0 );
-    Wlc_NtkTransferNames( pNtk, p->pNtk );
+    pNtk = Wlc_NtkDupDfs( p->pNtk, 0, 1 );
     pNtk->pSpec = Abc_UtilStrsav( pFileName );
 finish:
     Wlc_PrsPrintErrorMessage( p );
diff --git a/src/base/wlc/wlcShow.c b/src/base/wlc/wlcShow.c
index dd25c7a3..8ef21d29 100644
--- a/src/base/wlc/wlcShow.c
+++ b/src/base/wlc/wlcShow.c
@@ -143,7 +143,7 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
     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, "The word-level network contains %d nodes and spans %d levels.", Wlc_NtkObjNum(p)-Wlc_NtkCiNum(p), LevelMax-1 );
     fprintf( pFile, "\\n" );
     fprintf( pFile, "\"\n" );
     fprintf( pFile, "         ];\n" );
@@ -159,8 +159,9 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
     // 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" );
+        pNode = Wlc_ObjCo2PoFo(p, i);
+        fprintf( pFile, "  NodePo%d [label = \"%s_in %d\"", Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) ); 
+        fprintf( pFile, ", shape = %s", i < Wlc_NtkPoNum(p) ? "invtriangle" : "box" );
         fprintf( pFile, ", color = coral, fillcolor = coral" );
         fprintf( pFile, "];\n" );
     }
@@ -224,7 +225,7 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
     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, ", shape = %s", i < Wlc_NtkPiNum(p) ? "triangle" : "box" );
         fprintf( pFile, ", color = coral, fillcolor = coral" );
         fprintf( pFile, "];\n" );
     }
@@ -235,11 +236,15 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
     // generate invisible edges from the square down
     fprintf( pFile, "title1 -> title2 [style = invis];\n" );
     Wlc_NtkForEachCo( p, pNode, i )
+    {
+        pNode = Wlc_ObjCo2PoFo( p, 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 )
     {
+        pNode = Wlc_ObjCo2PoFo( p, i );
         if ( i > 0 )
             fprintf( pFile, "NodePo%d -> NodePo%d [style = invis];\n", Prev, Wlc_ObjId(p, pNode) );
         Prev = Wlc_ObjId(p, pNode);
@@ -254,22 +259,21 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
     }
 
     // generate edges
+    Wlc_NtkForEachCo( p, pNode, i )
+    {
+        fprintf( pFile, "NodePo%d",  Wlc_ObjId(p, Wlc_ObjCo2PoFo(p, i)) );
+        fprintf( pFile, " -> " );
+        fprintf( pFile, "Node%d",  Wlc_ObjId(p, pNode) );
+        fprintf( pFile, " [" );
+        fprintf( pFile, "style = %s", pNode->Signed? "dotted" : "solid" );
+        fprintf( pFile, "]" );
+        fprintf( pFile, ";\n" );
+    }
     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 )
         {
@@ -277,7 +281,9 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
             fprintf( pFile, " -> " );
             fprintf( pFile, "Node%d",  iFanin );
             fprintf( pFile, " [" );
-            fprintf( pFile, "style = %s", Wlc_NtkObj(p, iFanin)->Signed? "dotted" : "bold" );
+            fprintf( pFile, "style = %s", Wlc_NtkObj(p, iFanin)->Signed? "dotted" : "solid" );
+            if ( pNode->Type == WLC_OBJ_MUX && k == 0 )
+                fprintf( pFile, ", style = %s", "bold" );
             fprintf( pFile, "]" );
             fprintf( pFile, ";\n" );
         }
diff --git a/src/base/wlc/wlcWriteVer.c b/src/base/wlc/wlcWriteVer.c
index cf0e528f..c4dee094 100644
--- a/src/base/wlc/wlcWriteVer.c
+++ b/src/base/wlc/wlcWriteVer.c
@@ -409,7 +409,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops )
             fprintf( pFile, " reg%d (",       i );
             fprintf( pFile, " .q( %s ),",      Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
             fprintf( pFile, " .qbar()," );
-            fprintf( pFile, " .d( %s ),",      Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFoToFi(p, pObj))) );
+            fprintf( pFile, " .d( %s ),",      Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFo2Fi(p, pObj))) );
             fprintf( pFile, " .clk( %s ),",    "1\'b0" );
             fprintf( pFile, " .arst( %s ),",   "1\'b0" );
             if ( p->vInits )