Word-level abstraction.

8 files changed, 387 insertions, 14 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 321a6d71..f2fcf619 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -779,6 +779,10 @@ SOURCE=.\src\base\wlc\wlcAbs.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\wlc\wlcAbs2.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\wlc\wlcBlast.c
 # End Source File
 # Begin Source File
@@ -2071,6 +2075,10 @@ SOURCE=.\src\sat\satoko\utils\vec\vec_dble.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\satoko\utils\vec\vec_flt.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\satoko\utils\vec\vec_int.h
 # End Source File
 # Begin Source File
diff --git a/src/base/wlc/module.make b/src/base/wlc/module.make
index ae7899ec..3485bd4d 100644
--- a/src/base/wlc/module.make
+++ b/src/base/wlc/module.make
@@ -1,4 +1,5 @@
 SRC +=    src/base/wlc/wlcAbs.c \
+    src/base/wlc/wlcAbs2.c \
     src/base/wlc/wlcAbc.c \
     src/base/wlc/wlcBlast.c \
     src/base/wlc/wlcCom.c \
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index d51b699c..0a17cfe6 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -160,6 +160,16 @@ struct Wlc_Ntk_t_
     Vec_Int_t              vLevels;            // object levels
 };
 
+typedef struct Wlc_Par_t_ Wlc_Par_t;
+struct Wlc_Par_t_
+{
+    int                    nBitsAdd;           // adder bit-width
+    int                    nBitsMul;           // multiplier bit-widht 
+    int                    nBitsMux;           // MUX bit-width
+    int                    nBitsFlop;          // flop bit-width
+    int                    fVerbose;           // verbose output`
+};
+
 static inline int          Wlc_NtkObjNum( Wlc_Ntk_t * p )                           { return p->iObj - 1;                                                      }
 static inline int          Wlc_NtkObjNumMax( Wlc_Ntk_t * p )                        { return p->iObj;                                                          }
 static inline int          Wlc_NtkPiNum( Wlc_Ntk_t * p )                            { return Vec_IntSize(&p->vPis);                                            }
@@ -267,6 +277,9 @@ extern Vec_Int_t *    Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p );
 extern Vec_Int_t *    Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p );
 extern Wlc_Ntk_t *    Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes );
 extern Wlc_Ntk_t *    Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs );
+/*=== wlcAbs2.c ========================================================*/
+extern void           Wlc_ManSetDefaultParams( Wlc_Par_t * pPars );
+extern Wlc_Ntk_t *    Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
 /*=== wlcBlast.c ========================================================*/
 extern Gia_Man_t *    Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, int nRange, int fGiaSimple, int fAddOutputs, int fBooth );
 /*=== wlcCom.c ========================================================*/
@@ -291,7 +304,7 @@ extern void           Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type );
 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 Wlc_Ntk_t *    Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq, Vec_Int_t * vPisNew );
 extern void           Wlc_NtkCleanMarks( Wlc_Ntk_t * p );
 extern void           Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int Range, int fSeq, int fAllPis );
 extern void           Wlc_NtkProfileCones( Wlc_Ntk_t * p );
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index ce6b8de9..8662e509 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, 0, 1 );
+    pNew = Wlc_NtkDupDfs( p, 0, 1, NULL );
     return pNew;
 }
 
@@ -277,7 +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, 1 );
+    pNew = Wlc_NtkDupDfs( p, 0, 1, NULL );
     return pNew;
 }
 
diff --git a/src/base/wlc/wlcAbs2.c b/src/base/wlc/wlcAbs2.c
new file mode 100644
index 00000000..9da59f42
--- /dev/null
+++ b/src/base/wlc/wlcAbs2.c
@@ -0,0 +1,186 @@
+/**CFile****************************************************************
+
+  FileName    [wlcAbs2.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Abstraction for word-level networks.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 22, 2014.]
+
+  Revision    [$Id: wlcAbs2.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wlc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Wabs_Par_t_ Wabs_Par_t;
+struct Wabs_Par_t_
+{
+    Wlc_Ntk_t *            pNtk;
+    Wlc_Par_t *            pPars;
+    Vec_Bit_t *            vLeaves;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
+{
+    memset( pPars, 0, sizeof(Wlc_Par_t) );
+    pPars->nBitsAdd       =      16;  // adder bit-width
+    pPars->nBitsMul       =       8;  // multiplier bit-widht 
+    pPars->nBitsMux       =      32;  // MUX bit-width
+    pPars->nBitsFlop      =      32;  // flop bit-width
+    pPars->fVerbose       =       0;  // verbose output`
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Mark operators that meet the criteria.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+{
+    Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) );
+    Wlc_Obj_t * pObj; int i;
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd )
+                Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 );
+            continue;
+        }
+        if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul )
+                Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 );
+            continue;
+        }
+        if ( pObj->Type == WLC_OBJ_MUX )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux )
+                Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 );
+            continue;
+        }
+        if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop )
+                Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 );
+            continue;
+        }
+    }
+    return vLeaves;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeaves, Vec_Int_t * vFlops, Vec_Int_t * vPisNew )
+{
+    int i, iFanin;
+    if ( pObj->Mark )
+        return;
+    pObj->Mark = 1;
+    if ( Vec_BitEntry(vLeaves, Wlc_ObjId(p, pObj)) )
+    {
+        Vec_IntPush( vPisNew, Wlc_ObjId(p, pObj) );
+        return;
+    }
+    if ( Wlc_ObjIsCi(pObj) )
+    {
+        if ( !Wlc_ObjIsPi(pObj) )
+            Vec_IntPush( vFlops, Wlc_ObjCiId(pObj) );
+        return;
+    }
+    Wlc_ObjForEachFanin( pObj, iFanin, i )
+        Wlc_NtkAbsMarkNodes_rec( p, Wlc_NtkObj(p, iFanin), vLeaves, vFlops, vPisNew );
+}
+
+Vec_Int_t * Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves )
+{
+    Vec_Int_t * vFlops;
+    Vec_Int_t * vPisNew;
+    Wlc_Obj_t * pObj;
+    int i, CiId, CoId;
+    Wlc_NtkCleanMarks( p );
+    vFlops = Vec_IntAlloc( 100 );
+    vPisNew = Vec_IntAlloc( 100 );
+    Wlc_NtkForEachCo( p, pObj, i )
+        Wlc_NtkAbsMarkNodes_rec( p, pObj, vLeaves, vFlops, vPisNew );
+    Vec_IntForEachEntry( vFlops, CiId, i )
+    {
+        CoId = Wlc_NtkPoNum(p) + CiId - Wlc_NtkPiNum(p);
+        Wlc_NtkAbsMarkNodes_rec( p, Wlc_NtkCo(p, CoId), vLeaves, vFlops, vPisNew );
+    }
+    Vec_IntFree( vFlops );
+    return vPisNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+{
+    Vec_Bit_t * vLeaves = Wlc_NtkAbsMarkOpers( p, pPars );
+    Vec_Int_t * vPisNew = Wlc_NtkAbsMarkNodes( p, vLeaves );
+    Wlc_Ntk_t * pNtkNew = Wlc_NtkDupDfs( p, 1, 1, vPisNew );
+    Vec_IntFree( vPisNew );
+    Vec_BitFree( vLeaves );
+    return pNtkNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 82321d3b..3bbe843f 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -32,6 +32,7 @@ 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_CommandAbs        ( 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 );
@@ -72,6 +73,7 @@ void Wlc_Init( Abc_Frame_t * pAbc )
     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", "%abs",         Abc_CommandAbs,        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 );
@@ -421,7 +423,7 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
     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, Range, fSeq, fAllPis );
-    pNtk = Wlc_NtkDupDfs( pNtk, 1, fSeq );
+    pNtk = Wlc_NtkDupDfs( pNtk, 1, fSeq, NULL );
     ABC_FREE( pNtk->pName );
     pNtk->pName = Abc_UtilStrsav( pName );
     Wlc_AbcUpdateNtk( pAbc, pNtk );
@@ -449,6 +451,101 @@ usage:
   SeeAlso     []
 
 ******************************************************************************/
+int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    Wlc_Par_t Pars, * pPars = &Pars;
+    int c;
+    Wlc_ManSetDefaultParams( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'A':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBitsAdd = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBitsAdd < 0 )
+                goto usage;
+            break;
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBitsMul = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBitsMul < 0 )
+                goto usage;
+            break;
+        case 'X':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBitsMux = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBitsMux < 0 )
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBitsFlop = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBitsFlop < 0 )
+                goto usage;
+            break;
+        case 'v':
+            pPars->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;
+    }
+    pNtk = Wlc_NtkAbs( pNtk, pPars );
+    Wlc_AbcUpdateNtk( pAbc, pNtk );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%abs [-AMXF num] [-vh]\n" );
+    Abc_Print( -2, "\t         abstraction for word-level networks\n" );
+    Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
+    Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n",        pPars->nBitsMul );
+    Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n",      pPars->nBitsMux );
+    Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n",         pPars->nBitsFlop );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",                  pPars->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);
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index bd00a570..6eab4442 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -707,6 +707,45 @@ char * Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq )
 
 /**Function*************************************************************
 
+  Synopsis    [Reduce init vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Wlc_ReduceMarkedInitVec( Wlc_Ntk_t * p, Vec_Int_t * vInit )
+{
+    Vec_Int_t * vInitNew = Vec_IntDup( vInit );
+    Wlc_Obj_t * pObj; int i, k = 0;
+    assert( Vec_IntSize(vInit) == Wlc_NtkCiNum(p) - Wlc_NtkPiNum(p) );
+    Wlc_NtkForEachCi( p, pObj, i )
+        if ( !Wlc_ObjIsPi(pObj) && pObj->Mark )
+            Vec_IntWriteEntry( vInitNew, k++, Vec_IntEntry(vInit, i) );
+    Vec_IntShrink( vInitNew, k );
+    return vInitNew;
+}
+char * Wlc_ReduceMarkedInitStr( Wlc_Ntk_t * p, char * pInit )
+{
+    char * pInitNew = Abc_UtilStrsav( pInit );
+    Wlc_Obj_t * pObj; int i, b, nBits = 0, k = 0;
+    Wlc_NtkForEachCi( p, pObj, i )
+    {
+        if ( !Wlc_ObjIsPi(pObj) && pObj->Mark )
+            for ( b = 0; b < Wlc_ObjRange(pObj); b++ )
+                pInitNew[k++] = pInitNew[nBits+b];
+        if ( !Wlc_ObjIsPi(pObj) )
+            nBits += Wlc_ObjRange(pObj);
+    }
+    pInitNew[k] = '\0';
+    assert( nBits == (int)strlen(pInit) );
+    return pInitNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates the network in a topological order.]
 
   Description []
@@ -764,7 +803,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, int fMarked, int fSeq )
+Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq, Vec_Int_t * vPisNew )
 {
     Wlc_Ntk_t * pNew;
     Wlc_Obj_t * pObj;
@@ -774,14 +813,33 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq )
     Wlc_NtkCleanCopy( p );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
     pNew->fSmtLib = p->fSmtLib;
-    Wlc_NtkForEachCi( p, pObj, i )
-        if ( !fMarked || pObj->Mark )
+    if ( vPisNew )
+    {
+        // duplicate marked PIs
+        Wlc_NtkForEachPi( p, pObj, i )
+            if ( pObj->Mark )
+                Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+        // duplicated additional PIs
+        Wlc_NtkForEachObjVec( vPisNew, p, pObj, i )
         {
             unsigned Type = pObj->Type;
-            if ( !fSeq ) pObj->Type = WLC_OBJ_PI;
+            assert( !Wlc_ObjIsPi(pObj) );
+            pObj->Type = WLC_OBJ_PI;
             Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
             pObj->Type = Type;
         }
+    }
+    else
+    {
+        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 );
@@ -789,12 +847,22 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq )
         if ( !fMarked || pObj->Mark )
             Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), fSeq ? pObj->fIsFi : 0 );
     Vec_IntFree( vFanins );
-    if ( !fMarked )
+    if ( fSeq )
     {
-        if ( p->vInits )
-            pNew->vInits = Vec_IntDup( p->vInits );
-        if ( p->pInits )
-            pNew->pInits = Abc_UtilStrsav( p->pInits );
+        if ( fMarked )
+        {
+            if ( p->vInits )
+                pNew->vInits = Wlc_ReduceMarkedInitVec( p, p->vInits );
+            if ( p->pInits )
+                pNew->pInits = Wlc_ReduceMarkedInitStr( p, p->pInits );
+        }
+        else
+        {
+            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 );
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index e4a65ecf..f7546b5b 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, 0, 1 );
+    pNtk = Wlc_NtkDupDfs( p->pNtk, 0, 1, NULL );
     pNtk->pSpec = Abc_UtilStrsav( pFileName );
 finish:
     Wlc_PrsPrintErrorMessage( p );