Version abc70225

29 files changed, 3027 insertions, 1050 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index f638097f..c375a34e 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -316,6 +316,7 @@ static inline Abc_Obj_t * Abc_NtkCreatePo( Abc_Ntk_t * pNtk )        { return Ab
 static inline Abc_Obj_t * Abc_NtkCreateBi( Abc_Ntk_t * pNtk )        { return Abc_NtkCreateObj( pNtk, ABC_OBJ_BI );         }
 static inline Abc_Obj_t * Abc_NtkCreateBo( Abc_Ntk_t * pNtk )        { return Abc_NtkCreateObj( pNtk, ABC_OBJ_BO );         }
 static inline Abc_Obj_t * Abc_NtkCreateAssert( Abc_Ntk_t * pNtk )    { return Abc_NtkCreateObj( pNtk, ABC_OBJ_ASSERT );     }
+static inline Abc_Obj_t * Abc_NtkCreateNet( Abc_Ntk_t * pNtk )       { return Abc_NtkCreateObj( pNtk, ABC_OBJ_NET );        }
 static inline Abc_Obj_t * Abc_NtkCreateNode( Abc_Ntk_t * pNtk )      { return Abc_NtkCreateObj( pNtk, ABC_OBJ_NODE );       }
 static inline Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk )     { return Abc_NtkCreateObj( pNtk, ABC_OBJ_LATCH );      }
 static inline Abc_Obj_t * Abc_NtkCreateWhitebox( Abc_Ntk_t * pNtk )  { return Abc_NtkCreateObj( pNtk, ABC_OBJ_WHITEBOX );   }
@@ -535,6 +536,15 @@ extern void               Abc_AigUpdateStop( Abc_Aig_t * pMan );
 extern void               Abc_AigUpdateReset( Abc_Aig_t * pMan );
 /*=== abcAttach.c ==========================================================*/
 extern int                Abc_NtkAttach( Abc_Ntk_t * pNtk );
+/*=== abcBlifMv.c ==========================================================*/
+extern void               Abc_NtkStartMvVars( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkFreeMvVars( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkSetMvVarValues( Abc_Obj_t * pObj, int nValues );
+extern Abc_Ntk_t *        Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t *        Abc_NtkInsertBlifMv( Abc_Ntk_t * pNtkBase, Abc_Ntk_t * pNtkLogic );
+extern int                Abc_NtkConvertToBlifMv( Abc_Ntk_t * pNtk );
+extern char *             Abc_NodeConvertSopToMvSop( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 );
+extern int                Abc_NodeEvalMvCost( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 );
 /*=== abcBalance.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective, bool fUpdateLevel );
 /*=== abcCheck.c ==========================================================*/
@@ -544,6 +554,9 @@ extern bool               Abc_NtkDoCheck( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
 extern bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOnlyPis, int fComb );
 extern int                Abc_NtkIsAcyclicHierarchy( Abc_Ntk_t * pNtk );
+extern int                Abc_NtkCheckUniqueCiNames( Abc_Ntk_t * pNtk );
+extern int                Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk );
+extern int                Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk );
 /*=== abcCollapse.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose );
 /*=== abcCut.c ==========================================================*/
@@ -616,6 +629,7 @@ extern void               Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk );
 extern void               Abc_LibPrint( Abc_Lib_t * pLib );
 extern int                Abc_LibAddModel( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_LibFindModelByName( Abc_Lib_t * pLib, char * pName );
+extern int                Abc_LibFindTopLevelModels( Abc_Lib_t * pLib );
 extern Abc_Ntk_t *        Abc_LibDeriveRoot( Abc_Lib_t * pLib );
 /*=== abcMiter.c ==========================================================*/
 extern int                Abc_NtkMinimumBase( Abc_Ntk_t * pNtk );
@@ -682,7 +696,7 @@ extern void               Abc_NtkAddDummyBoxNames( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkShortNames( Abc_Ntk_t * pNtk );
 /*=== abcNetlist.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkToLogic( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkToNetlist( Abc_Ntk_t * pNtk, int fDirect );
+extern Abc_Ntk_t *        Abc_NtkToNetlist( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkToNetlistBench( Abc_Ntk_t * pNtk );
 /*=== abcNtbdd.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi );
@@ -783,6 +797,10 @@ extern int                Abc_SopIsExorType( char * pSop );
 extern bool               Abc_SopCheck( char * pSop, int nFanins );
 extern char *             Abc_SopFromTruthBin( char * pTruth );
 extern char *             Abc_SopFromTruthHex( char * pTruth );
+extern char *             Abc_SopEncoderPos( Extra_MmFlex_t * pMan, int iValue, int nValues );
+extern char *             Abc_SopEncoderLog( Extra_MmFlex_t * pMan, int iBit, int nValues );
+extern char *             Abc_SopDecoderPos( Extra_MmFlex_t * pMan, int nValues );
+extern char *             Abc_SopDecoderLog( Extra_MmFlex_t * pMan, int nValues );
 /*=== abcStrash.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup );
 extern Abc_Obj_t *        Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode );
diff --git a/src/base/abc/abcBlifMv.c b/src/base/abc/abcBlifMv.c
new file mode 100644
index 00000000..48ec58c0
--- /dev/null
+++ b/src/base/abc/abcBlifMv.c
@@ -0,0 +1,970 @@
+/**CFile****************************************************************
+
+  FileName    [abcBlifMv.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Procedures to process BLIF-MV networks and AIGs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcBlifMv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the Mv-Var manager.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkStartMvVars( Abc_Ntk_t * pNtk ) 
+{
+    Vec_Att_t * pAttMan;
+    assert( Abc_NtkMvVar(pNtk) == NULL );
+    pAttMan = Vec_AttAlloc( 0, Abc_NtkObjNumMax(pNtk) + 1, Extra_MmFlexStart(), Extra_MmFlexStop, NULL, NULL );
+    Vec_PtrWriteEntry( pNtk->vAttrs, VEC_ATTR_MVVAR, pAttMan );
+//printf( "allocing attr\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the Mv-Var manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFreeMvVars( Abc_Ntk_t * pNtk ) 
+{ 
+    void * pUserMan;
+    pUserMan = Abc_NtkAttrFree( pNtk, VEC_ATTR_GLOBAL_BDD, 0 ); 
+    Extra_MmFlexStop( pUserMan );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicate the MV variable.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSetMvVarValues( Abc_Obj_t * pObj, int nValues )
+{
+    Extra_MmFlex_t * pFlex;
+    struct temp 
+    { 
+        int nValues; 
+        char ** pNames; 
+    } * pVarStruct;
+    assert( nValues > 1 );
+    // skip binary signals
+    if ( nValues == 2 )
+        return;
+    // skip already assigned signals
+    if ( Abc_ObjMvVar(pObj) != NULL )
+        return;
+    // create the structure
+    pFlex = Abc_NtkMvVarMan( pObj->pNtk );
+    pVarStruct = (void *)Extra_MmFlexEntryFetch( pFlex, sizeof(struct temp) );
+    pVarStruct->nValues = nValues;
+    pVarStruct->pNames = NULL;
+    Abc_ObjSetMvVar( pObj, pVarStruct );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes the BLIF-MV netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_StringGetNumber( char ** ppStr )
+{
+    char * pStr = *ppStr;
+    int Number = 0;
+    assert( *pStr >= '0' && *pStr <= '9' );
+    for ( ; *pStr >= '0' && *pStr <= '9'; pStr++ )
+        Number = 10 * Number + *pStr - '0';
+    *ppStr = pStr;
+    return Number;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes one node in the BLIF-MV netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeStrashBlifMv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
+{
+    char * pSop;
+    Abc_Obj_t ** pValues, ** pValuesF, ** pValuesF2;
+    Abc_Obj_t * pTemp, * pTemp2, * pFanin, * pFanin2, * pNet;
+    int k, v, Def, DefIndex, Index, nValues, nValuesF, nValuesF2;
+
+    // start the output values
+    assert( Abc_ObjIsNode(pObj) );
+    pNet = Abc_ObjFanout0(pObj);
+    nValues = Abc_ObjMvVarNum(pNet);
+    pValues = ALLOC( Abc_Obj_t *, nValues );
+    for ( k = 0; k < nValues; k++ )
+        pValues[k] = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
+
+    // get the BLIF-MV formula
+    pSop = pObj->pData;
+    // skip the value line
+//    while ( *pSop++ != '\n' );
+
+    // handle the constant
+    if ( Abc_ObjFaninNum(pObj) == 0 )
+    {
+        // skip the default if present
+        if ( *pSop == 'd' )
+            while ( *pSop++ != '\n' );
+        // skip space if present
+        if ( *pSop == ' ' )
+            pSop++;
+        Index = Abc_StringGetNumber( &pSop );
+        assert( Index < nValues );
+        pValues[Index] = Abc_AigConst1(pNtkNew);
+        // save the values in the fanout net
+        pNet->pCopy = (Abc_Obj_t *)pValues;
+        return 1;
+    }
+
+    // parse the default line
+    Def = DefIndex = -1;
+    if ( *pSop == 'd' )
+    {
+        pSop++;
+        if ( *pSop == '=' )
+        {
+            pSop++;
+            DefIndex = Abc_StringGetNumber( &pSop );
+            assert( DefIndex < Abc_ObjFaninNum(pObj) );
+        }
+        else if ( *pSop == '-' )
+        {
+            pSop++;
+            Def = 0;
+        }
+        else
+        {
+            Def = Abc_StringGetNumber( &pSop );
+            assert( Def < nValues );
+        }
+        assert( *pSop == '\n' );
+        pSop++;
+    }
+
+    // convert the values
+    while ( *pSop )
+    {
+        // extract the values for each cube
+        pTemp = Abc_AigConst1(pNtkNew); 
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            if ( *pSop == '-' )
+            {
+                pSop += 2;
+                continue;
+            }
+            if ( *pSop == '!' )
+            {
+                printf( "Abc_NodeStrashBlifMv(): Cannot handle complement in the MV function of node %s.\n", Abc_ObjName(Abc_ObjFanout0(pObj)) );
+                return 0;
+            }
+            if ( *pSop == '{' )
+            {
+                printf( "Abc_NodeStrashBlifMv(): Cannot handle braces in the MV function of node %s.\n", Abc_ObjName(Abc_ObjFanout0(pObj)) );
+                return 0;
+            }
+            // get the value set
+            nValuesF = Abc_ObjMvVarNum(pFanin);
+            pValuesF = (Abc_Obj_t **)pFanin->pCopy;
+            if ( *pSop == '(' )
+            {
+                pSop++;
+                pTemp2 = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
+                while ( *pSop != ')' )
+                {
+                    Index = Abc_StringGetNumber( &pSop );
+                    assert( Index < nValuesF );
+                    pTemp2 = Abc_AigOr( pNtkNew->pManFunc, pTemp2, pValuesF[Index] );
+                    assert( *pSop == ')' || *pSop == ',' );
+                    if ( *pSop == ',' )
+                        pSop++;
+                }
+                assert( *pSop == ')' );
+                pSop++;
+            }
+            else if ( *pSop == '=' )
+            {
+                pSop++;
+                // get the fanin index
+                Index = Abc_StringGetNumber( &pSop );
+                assert( Index < Abc_ObjFaninNum(pObj) );
+                assert( Index != k );
+                // get the fanin
+                pFanin2 = Abc_ObjFanin( pObj, Index );
+                nValuesF2 = Abc_ObjMvVarNum(pFanin2);
+                pValuesF2 = (Abc_Obj_t **)pFanin2->pCopy;
+                // create the sum of products of values
+                assert( nValuesF == nValuesF2 );
+                pTemp2 = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
+                for ( v = 0; v < nValues; v++ )
+                    pTemp2 = Abc_AigOr( pNtkNew->pManFunc, pTemp2, Abc_AigAnd(pNtkNew->pManFunc, pValuesF[v], pValuesF2[v]) );
+            }
+            else
+            {
+                Index = Abc_StringGetNumber( &pSop );
+                assert( Index < nValuesF );
+                pTemp2 = pValuesF[Index];
+            }
+            // compute the compute
+            pTemp = Abc_AigAnd( pNtkNew->pManFunc, pTemp, pTemp2 );
+            // advance the reading point
+            assert( *pSop == ' ' );
+            pSop++;
+        }
+        // check if the output value is an equal construct
+        if ( *pSop == '=' )
+        {
+            pSop++;
+            // get the output value
+            Index = Abc_StringGetNumber( &pSop );
+            assert( Index < Abc_ObjFaninNum(pObj) );
+            // add values of the given fanin with the given cube
+            pFanin = Abc_ObjFanin( pObj, Index );
+            nValuesF = Abc_ObjMvVarNum(pFanin);
+            pValuesF = (Abc_Obj_t **)pFanin->pCopy;
+            assert( nValuesF == nValues ); // should be guaranteed by the parser
+            for ( k = 0; k < nValuesF; k++ )
+                pValues[k] = Abc_AigOr( pNtkNew->pManFunc, pValues[k], Abc_AigAnd(pNtkNew->pManFunc, pTemp, pValuesF[k]) );
+        }
+        else
+        {
+            // get the output value
+            Index = Abc_StringGetNumber( &pSop );
+            assert( Index < nValues );
+            pValues[Index] = Abc_AigOr( pNtkNew->pManFunc, pValues[Index], pTemp );
+        }
+        // advance the reading point
+        assert( *pSop == '\n' );
+        pSop++;
+    }
+
+    // compute the default value
+    if ( Def >= 0 || DefIndex >= 0 )
+    {
+        pTemp = Abc_AigConst1(pNtkNew);
+        for ( k = 0; k < nValues; k++ )
+        {
+            if ( k == Def )
+                continue;
+            pTemp = Abc_AigAnd( pNtkNew->pManFunc, pTemp, Abc_ObjNot(pValues[k]) );
+        }
+
+        // assign the default value
+        if ( Def >= 0 )
+            pValues[Def] = pTemp;
+        else
+        {
+            assert( DefIndex >= 0 );
+            // add values of the given fanin with the given cube
+            pFanin = Abc_ObjFanin( pObj, DefIndex );
+            nValuesF = Abc_ObjMvVarNum(pFanin);
+            pValuesF = (Abc_Obj_t **)pFanin->pCopy;
+            assert( nValuesF == nValues ); // should be guaranteed by the parser
+            for ( k = 0; k < nValuesF; k++ )
+                pValues[k] = Abc_AigOr( pNtkNew->pManFunc, pValues[k], Abc_AigAnd(pNtkNew->pManFunc, pTemp, pValuesF[k]) );
+        }
+
+    }
+
+    // save the values in the fanout net
+    pNet->pCopy = (Abc_Obj_t *)pValues;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Assigns name with index.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_NtkConvertAssignName( Abc_Obj_t * pObj, Abc_Obj_t * pNet, int Index )
+{
+    char Suffix[16];
+    assert( Abc_ObjIsTerm(pObj) );
+    assert( Abc_ObjIsNet(pNet) );
+    sprintf( Suffix, "[%d]", Index );
+    Abc_ObjAssignName( pObj, Abc_ObjName(pNet), Suffix );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes the BLIF-MV netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
+{
+    int fUsePositional = 0;
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t ** pBits;
+    Abc_Obj_t ** pValues;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj, * pTemp, * pBit, * pNet;
+    int i, k, v, nValues, nValuesMax, nBits;
+
+    assert( Abc_NtkIsNetlist(pNtk) );
+    assert( Abc_NtkHasBlifMv(pNtk) );
+    assert( Abc_NtkWhiteboxNum(pNtk) == 0 );
+    assert( Abc_NtkBlackboxNum(pNtk) == 0 );
+
+    // get the largest number of values
+    nValuesMax = 2;
+    Abc_NtkForEachNet( pNtk, pObj, i )
+    {
+        nValues = Abc_ObjMvVarNum(pObj);
+        if ( nValuesMax < nValues )
+            nValuesMax = nValues;
+    }
+    nBits = Extra_Base2Log( nValuesMax );
+    pBits = ALLOC( Abc_Obj_t *, nBits );
+
+    // clean the node copy fields
+    Abc_NtkCleanCopy( pNtk );
+    // collect the nodes
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+
+    // start the network
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+    // duplicate the name and the spec
+    pNtkNew->pName = Extra_UtilStrsav( pNtk->pName );
+//    pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pName );
+
+    // encode the CI nets
+    Abc_NtkIncrementTravId( pNtk );
+    if ( fUsePositional )
+    {
+        Abc_NtkForEachCi( pNtk, pObj, i )
+        {
+            pNet = Abc_ObjFanout0(pObj);
+            nValues = Abc_ObjMvVarNum(pNet);
+            pValues = ALLOC( Abc_Obj_t *, nValues );
+            // create PIs for the values
+            for ( v = 0; v < nValues; v++ )
+            {
+                pValues[v] = Abc_NtkCreatePi( pNtkNew );
+                Abc_NtkConvertAssignName( pValues[v], pNet, v );
+            }
+            // save the values in the fanout net
+            pNet->pCopy = (Abc_Obj_t *)pValues;
+            // mark the net
+            Abc_NodeSetTravIdCurrent( pNet );
+        }
+    }
+    else
+    {
+        Abc_NtkForEachCi( pNtk, pObj, i )
+        {
+            pNet = Abc_ObjFanout0(pObj);
+            nValues = Abc_ObjMvVarNum(pNet);
+            pValues = ALLOC( Abc_Obj_t *, nValues );
+            // create PIs for the encoding bits
+            nBits = Extra_Base2Log( nValues );
+            for ( k = 0; k < nBits; k++ )
+            {
+                pBits[k] = Abc_NtkCreatePi( pNtkNew );
+                Abc_NtkConvertAssignName( pBits[k], pNet, k );
+            }
+            // encode the values
+            for ( v = 0; v < nValues; v++ )
+            {
+                pValues[v] = Abc_AigConst1(pNtkNew);
+                for ( k = 0; k < nBits; k++ )
+                {
+                    pBit = Abc_ObjNotCond( pBits[k], (v&(1<<k)) == 0 );
+                    pValues[v] = Abc_AigAnd( pNtkNew->pManFunc, pValues[v], pBit );
+                }
+            }
+            // save the values in the fanout net
+            pNet->pCopy = (Abc_Obj_t *)pValues;
+            // mark the net
+            Abc_NodeSetTravIdCurrent( pNet );
+        }
+    }
+
+    // process nodes in the topological order
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        if ( !Abc_NodeStrashBlifMv( pNtkNew, pObj ) )
+        {
+            Abc_NtkDelete( pNtkNew );
+            return NULL;
+        }
+    Vec_PtrFree( vNodes );
+
+    // encode the CO nets
+    if ( fUsePositional )
+    {
+        Abc_NtkForEachCo( pNtk, pObj, i )
+        {
+            pNet = Abc_ObjFanin0(pObj);
+            // skip marked nets
+            if ( Abc_NodeIsTravIdCurrent(pNet) )
+                continue;
+            Abc_NodeSetTravIdCurrent( pNet );
+            nValues = Abc_ObjMvVarNum(pNet);
+            pValues = (Abc_Obj_t **)pNet->pCopy;
+            for ( v = 0; v < nValues; v++ )
+            {
+                pTemp = Abc_NtkCreatePo( pNtkNew );
+                Abc_ObjAddFanin( pTemp, pValues[v] );
+                Abc_NtkConvertAssignName( pTemp, pNet, v );
+            }
+        }
+    }
+    else
+    {
+        Abc_NtkForEachCo( pNtk, pObj, i )
+        {
+            pNet = Abc_ObjFanin0(pObj);
+            // skip marked nets
+            if ( Abc_NodeIsTravIdCurrent(pNet) )
+                continue;
+            Abc_NodeSetTravIdCurrent( pNet );
+            nValues = Abc_ObjMvVarNum(pNet);
+            pValues = (Abc_Obj_t **)pNet->pCopy;
+            nBits = Extra_Base2Log( nValues );
+            for ( k = 0; k < nBits; k++ )
+            {
+                pBit = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
+                for ( v = 0; v < nValues; v++ )
+                    if ( v & (1<<k) )
+                        pBit = Abc_AigOr( pNtkNew->pManFunc, pBit, pValues[v] );
+                pTemp = Abc_NtkCreatePo( pNtkNew );
+                Abc_ObjAddFanin( pTemp, pBit );
+                Abc_NtkConvertAssignName( pTemp, pNet, k );
+            }
+        }
+    }
+
+    // cleanup
+    free( pBits );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( pObj->pCopy )
+            free( pObj->pCopy );
+
+    // remove dangling nodes
+    i = Abc_AigCleanup(pNtkNew->pManFunc);
+//    printf( "Cleanup removed %d nodes.\n", i );
+//    Abc_NtkReassignIds( pNtkNew );
+
+    // check integrity
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        fprintf( stdout, "Abc_NtkStrashBlifMv(): Network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Extract the MV-skeleton of the BLIF-MV network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkSkeletonBlifMv( Abc_Ntk_t * pNtk )
+{
+    int fUsePositional = 0;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj, * pNet, * pNetNew, * pNodeNew, * pTermNew, * pBoxNew;
+    int i, k, v, nValues, nBits;
+
+    assert( Abc_NtkIsNetlist(pNtk) );
+    assert( Abc_NtkHasBlifMv(pNtk) );
+    assert( Abc_NtkWhiteboxNum(pNtk) == 0 );
+    assert( Abc_NtkBlackboxNum(pNtk) == 0 );
+
+    // clean the node copy fields
+    Abc_NtkCleanCopy( pNtk );
+
+    // start the network
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
+    // duplicate the name and the spec
+    pNtkNew->pName = Extra_UtilStrsav( pNtk->pName );
+    pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pName );
+    // create the internal box (it is important to put it first!)
+    pBoxNew = Abc_NtkCreateWhitebox( pNtkNew );
+    // create PIs and their nets
+    Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+        Abc_NtkDupObj( pNtkNew, pObj, 0 );
+        pNet = Abc_ObjFanout0(pObj);
+        Abc_NtkDupObj( pNtkNew, pNet, 1 );
+        Abc_ObjAddFanin( pNet->pCopy, pObj->pCopy );
+    }
+    // create POs and their nets
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        Abc_NtkDupObj( pNtkNew, pObj, 0 );
+        pNet = Abc_ObjFanin0(pObj);
+        if ( pNet->pCopy == NULL )
+            Abc_NtkDupObj( pNtkNew, pNet, 1 );
+        Abc_ObjAddFanin( pObj->pCopy, pNet->pCopy );
+    }
+    // create latches
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        Abc_NtkDupBox( pNtkNew, pObj, 0 );
+        // latch outputs
+        pNet = Abc_ObjFanout0(Abc_ObjFanout0(pObj));
+        assert( pNet->pCopy == NULL );
+        Abc_NtkDupObj( pNtkNew, pNet, 1 );
+        Abc_ObjAddFanin( pNet->pCopy, Abc_ObjFanout0(pObj)->pCopy );
+        // latch inputs
+        pNet = Abc_ObjFanin0(Abc_ObjFanin0(pObj));
+        if ( pNet->pCopy == NULL )
+            Abc_NtkDupObj( pNtkNew, pNet, 1 );
+        Abc_ObjAddFanin( Abc_ObjFanin0(pObj)->pCopy, pNet->pCopy );
+    }
+
+    // encode the CI nets
+    Abc_NtkIncrementTravId( pNtk );
+    if ( fUsePositional )
+    {
+        Abc_NtkForEachCi( pNtk, pObj, i )
+        {
+            pNet = Abc_ObjFanout0(pObj);
+            nValues = Abc_ObjMvVarNum(pNet);
+            for ( v = 0; v < nValues; v++ )
+            {
+                pNodeNew = Abc_NtkCreateNode( pNtkNew );
+                pNodeNew->pData = Abc_SopEncoderPos( pNtkNew->pManFunc, v, nValues );
+                pNetNew = Abc_NtkCreateNet( pNtkNew );
+                pTermNew = Abc_NtkCreateBi( pNtkNew );
+                Abc_ObjAddFanin( pNodeNew, pNet->pCopy );
+                Abc_ObjAddFanin( pNetNew, pNodeNew );
+                Abc_ObjAddFanin( pTermNew, pNetNew );
+                Abc_ObjAddFanin( pBoxNew, pTermNew );
+            }
+            // mark the net
+            Abc_NodeSetTravIdCurrent( pNet );
+        }
+    }
+    else
+    {
+        Abc_NtkForEachCi( pNtk, pObj, i )
+        {
+            pNet = Abc_ObjFanout0(pObj);
+            nValues = Abc_ObjMvVarNum(pNet);
+            nBits = Extra_Base2Log( nValues );
+            for ( k = 0; k < nBits; k++ )
+            {
+                pNodeNew = Abc_NtkCreateNode( pNtkNew );
+                pNodeNew->pData = Abc_SopEncoderLog( pNtkNew->pManFunc, k, nValues );
+                pNetNew = Abc_NtkCreateNet( pNtkNew );
+                pTermNew = Abc_NtkCreateBi( pNtkNew );
+                Abc_ObjAddFanin( pNodeNew, pNet->pCopy );
+                Abc_ObjAddFanin( pNetNew, pNodeNew );
+                Abc_ObjAddFanin( pTermNew, pNetNew );
+                Abc_ObjAddFanin( pBoxNew, pTermNew );
+            }
+            // mark the net
+            Abc_NodeSetTravIdCurrent( pNet );
+        }
+    }
+
+    // encode the CO nets
+    if ( fUsePositional )
+    {
+        Abc_NtkForEachCo( pNtk, pObj, i )
+        {
+            pNet = Abc_ObjFanin0(pObj);
+            // skip marked nets
+            if ( Abc_NodeIsTravIdCurrent(pNet) )
+                continue;
+            Abc_NodeSetTravIdCurrent( pNet );
+            nValues = Abc_ObjMvVarNum(pNet);
+            pNodeNew = Abc_NtkCreateNode( pNtkNew );
+            pNodeNew->pData = Abc_SopDecoderPos( pNtkNew->pManFunc, nValues );
+            for ( v = 0; v < nValues; v++ )
+            {
+                pTermNew = Abc_NtkCreateBo( pNtkNew );
+                pNetNew = Abc_NtkCreateNet( pNtkNew );
+                Abc_ObjAddFanin( pTermNew, pBoxNew );
+                Abc_ObjAddFanin( pNetNew, pTermNew );
+                Abc_ObjAddFanin( pNodeNew, pNetNew );
+            }
+            Abc_ObjAddFanin( pNet->pCopy, pNodeNew );
+        }
+    }
+    else
+    {
+        Abc_NtkForEachCo( pNtk, pObj, i )
+        {
+            pNet = Abc_ObjFanin0(pObj);
+            // skip marked nets
+            if ( Abc_NodeIsTravIdCurrent(pNet) )
+                continue;
+            Abc_NodeSetTravIdCurrent( pNet );
+            nValues = Abc_ObjMvVarNum(pNet);
+            nBits = Extra_Base2Log( nValues );
+            pNodeNew = Abc_NtkCreateNode( pNtkNew );
+            pNodeNew->pData = Abc_SopDecoderLog( pNtkNew->pManFunc, nValues );
+            for ( k = 0; k < nBits; k++ )
+            {
+                pTermNew = Abc_NtkCreateBo( pNtkNew );
+                pNetNew = Abc_NtkCreateNet( pNtkNew );
+                Abc_ObjAddFanin( pTermNew, pBoxNew );
+                Abc_ObjAddFanin( pNetNew, pTermNew );
+                Abc_ObjAddFanin( pNodeNew, pNetNew );
+            }
+            Abc_ObjAddFanin( pNet->pCopy, pNodeNew );
+        }
+    }
+
+    // if it is a BLIF-MV netlist transfer the values of all nets
+    if ( Abc_NtkHasBlifMv(pNtk) && Abc_NtkMvVar(pNtk) )
+    {
+        if ( Abc_NtkMvVar( pNtkNew ) == NULL )
+            Abc_NtkStartMvVars( pNtkNew );
+        Abc_NtkForEachNet( pNtk, pObj, i )
+            if ( pObj->pCopy )
+                Abc_NtkSetMvVarValues( pObj->pCopy, Abc_ObjMvVarNum(pObj) );
+    }
+
+    // check integrity
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        fprintf( stdout, "Abc_NtkSkeletonBlifMv(): Network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts processed network into original base MV network.]
+
+  Description [The original network remembers the interface of combinational 
+  logic (PIs/POs/latches names and values). The processed network may 
+  be binary or multi-valued (currently, multi-value is not supported). 
+  The resulting network has the same interface as the original network 
+  while the internal logic is the same as that of the processed network.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkInsertBlifMv( Abc_Ntk_t * pNtkBase, Abc_Ntk_t * pNtkLogic )
+{
+    Abc_Ntk_t * pNtkSkel, * pNtkNew;
+    Abc_Obj_t * pBox;
+
+    assert( Abc_NtkIsNetlist(pNtkBase) );
+    assert( Abc_NtkHasBlifMv(pNtkBase) );
+    assert( Abc_NtkWhiteboxNum(pNtkBase) == 0 );
+    assert( Abc_NtkBlackboxNum(pNtkBase) == 0 );
+
+    assert( Abc_NtkIsNetlist(pNtkLogic) );
+    assert( Abc_NtkHasBlifMv(pNtkLogic) );
+    assert( Abc_NtkWhiteboxNum(pNtkLogic) == 0 );
+    assert( Abc_NtkBlackboxNum(pNtkLogic) == 0 );
+
+    // extract the skeleton of the old network
+    pNtkSkel = Abc_NtkSkeletonBlifMv( pNtkBase );
+
+    // set the implementation of the box to be the same as the processed network
+    assert( Abc_NtkWhiteboxNum(pNtkSkel) == 1 );
+    pBox = Abc_NtkBox( pNtkSkel, 0 );
+    assert( Abc_ObjIsWhitebox(pBox) );
+    assert( pBox->pData == NULL );
+    assert( Abc_ObjFaninNum(pBox) == Abc_NtkPiNum(pNtkLogic) );
+    assert( Abc_ObjFanoutNum(pBox) == Abc_NtkPoNum(pNtkLogic) );
+    pBox->pData = pNtkLogic;
+
+    // flatten the hierarchy to insert the processed network
+    pNtkNew = Abc_NtkFlattenLogicHierarchy( pNtkSkel );
+    pBox->pData = NULL;
+    Abc_NtkDelete( pNtkSkel );
+    return pNtkNew;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts SOP netlist into BLIF-MV netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkConvertToBlifMv( Abc_Ntk_t * pNtk )
+{
+    Extra_MmFlex_t * pMmFlex;
+    Abc_Obj_t * pNode;
+    Vec_Str_t * vCube;
+    char * pSop0, * pSop1, * pBlifMv, * pCube, * pCur;
+    int Value, nCubes, nSize, i, k;
+
+    assert( Abc_NtkIsNetlist(pNtk) );
+    if ( !Abc_NtkToBdd(pNtk) )
+    {
+        printf( "Converting logic functions to BDDs has failed.\n" );
+        return 0;
+    }
+
+    pMmFlex = Extra_MmFlexStart();
+    vCube   = Vec_StrAlloc( 100 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // convert BDD into cubes for on-set and off-set
+        Abc_NodeBddToCnf( pNode, pMmFlex, vCube, 0, &pSop0, &pSop1 );
+        // allocate room for the MV-SOP
+        nCubes = Abc_SopGetCubeNum(pSop0) + Abc_SopGetCubeNum(pSop1);
+        nSize = nCubes*(2*Abc_ObjFaninNum(pNode) + 2)+1;
+        pBlifMv = Extra_MmFlexEntryFetch( pMmFlex, nSize );
+        // add the cubes
+        pCur = pBlifMv;
+        Abc_SopForEachCube( pSop0, Abc_ObjFaninNum(pNode), pCube )
+        {
+            Abc_CubeForEachVar( pCube, Value, k )
+            {
+                *pCur++ = Value;
+                *pCur++ = ' ';
+            }
+            *pCur++ = '0';
+            *pCur++ = '\n';
+        }
+        Abc_SopForEachCube( pSop1, Abc_ObjFaninNum(pNode), pCube )
+        {
+            Abc_CubeForEachVar( pCube, Value, k )
+            {
+                *pCur++ = Value;
+                *pCur++ = ' ';
+            }
+            *pCur++ = '1';
+            *pCur++ = '\n';
+        }
+        *pCur++ = 0;
+        assert( pCur - pBlifMv == nSize );
+        // update the node representation
+        Cudd_RecursiveDeref( pNtk->pManFunc, pNode->pData );
+        pNode->pData = pBlifMv;
+    }
+
+    // update the functionality type
+    pNtk->ntkFunc = ABC_FUNC_BLIFMV;
+    Cudd_Quit( pNtk->pManFunc );
+    pNtk->pManFunc = pMmFlex;
+
+    Vec_StrFree( vCube );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts SOP into MV-SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_NodeConvertSopToMvSop( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 )
+{
+    char * pMvSop, * pCur;
+    unsigned uCube;
+    int nCubes, nSize, Value, i, k;
+    // consider the case of the constant node
+    if ( Vec_IntSize(vSop0) == 0 || Vec_IntSize(vSop1) == 0 )
+    {
+        // (temporary) create a tautology cube
+        pMvSop = ALLOC( char, nVars + 3 );
+        for ( k = 0; k < nVars; k++ )
+            pMvSop[k] = '-';
+        pMvSop[nVars] = '0' + (int)(Vec_IntSize(vSop1) > 0);
+        pMvSop[nVars+1] = '\n';
+        pMvSop[nVars+2] = 0;
+        return pMvSop;
+    }
+    // find the total number of cubes
+    nCubes = Vec_IntSize(vSop0) + Vec_IntSize(vSop1);
+    // find the size of the MVSOP represented as a C-string
+    // (each cube has nVars variables + one output literal + end-of-line,
+    // and the string is zero-terminated)
+    nSize = nCubes * (nVars + 2) + 1; 
+    // allocate memory
+    pMvSop = pCur = ALLOC( char, nSize );
+    // fill in the negative polarity cubes
+    Vec_IntForEachEntry( vSop0, uCube, i )
+    {
+        for ( k = 0; k < nVars; k++ )
+        {
+            Value = (uCube >> (2*k)) & 3;
+            if ( Value == 1 )
+                *pCur++ = '0';
+            else if ( Value == 2 )
+                *pCur++ = '1';
+            else if ( Value == 0 )
+                *pCur++ = '-';
+            else
+                assert( 0 );
+        }
+        *pCur++ = '0';
+        *pCur++ = '\n';
+    }
+    // fill in the positive polarity cubes
+    Vec_IntForEachEntry( vSop1, uCube, i )
+    {
+        for ( k = 0; k < nVars; k++ )
+        {
+            Value = (uCube >> (2*k)) & 3;
+            if ( Value == 1 )
+                *pCur++ = '0';
+            else if ( Value == 2 )
+                *pCur++ = '1';
+            else if ( Value == 0 )
+                *pCur++ = '-';
+            else
+                assert( 0 );
+        }
+        *pCur++ = '1';
+        *pCur++ = '\n';
+    }
+    *pCur++ = 0;
+    assert( pCur - pMvSop == nSize );
+    return pMvSop;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [A prototype of internal cost evaluation procedure.]
+
+  Description [This procedure takes the number of variables (nVars),
+  the array of values of the inputs and the output (pVarValues) 
+  (note that this array has nVars+1 entries), and an MV-SOP represented
+  as a C-string with one charater for each literal, including inputs
+  and output. Each cube is terminated with the new-line character ('\n').
+  The string is zero-terminated.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeEvalMvCostInternal( int nVars, int * pVarValues, char * pMvSop ) 
+{
+    // for now, return the number of cubes in the MV-SOP
+    int Counter = 0;
+    while ( *pMvSop ) Counter += (*pMvSop++ == '\n');
+    return Counter;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluates the cost of the cut.]
+
+  Description [The Boolean function of the cut is specified by two SOPs, 
+  which represent the negative/positive polarities of the cut function.
+  Converts these two SOPs into a mutually-agreed-upon representation 
+  to be passed to the internal cost-evaluation procedure (see the above
+  prototype Abc_NodeEvalMvCostInternal).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeEvalMvCost( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 ) 
+{
+    char * pMvSop;
+    int * pVarValues;
+    int i, RetValue;
+    // collect the input and output values (currently, they are binary)
+    pVarValues = ALLOC( int, nVars + 1 );
+    for ( i = 0; i <= nVars; i++ )
+        pVarValues[i] = 2;
+    // prepare MV-SOP for evaluation
+    pMvSop = Abc_NodeConvertSopToMvSop( nVars, vSop0, vSop1 );
+    // have a look at the MV-SOP:
+//    printf( "%s\n", pMvSop );
+    // get the result of internal cost evaluation
+    RetValue = Abc_NodeEvalMvCostInternal( nVars, pVarValues, pMvSop );
+    // cleanup
+    free( pVarValues );
+    free( pMvSop );
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index e159bcab..24f10475 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -277,6 +277,19 @@ bool Abc_NtkCheckNames( Abc_Ntk_t * pNtk )
         }
     }
     Vec_IntFree( vNameIds );
+
+    // make sure the CI names are unique
+    if ( !Abc_NtkCheckUniqueCiNames(pNtk) )
+        return 0;
+
+    // make sure the CO names are unique
+    if ( !Abc_NtkCheckUniqueCoNames(pNtk) )
+        return 0;
+
+    // make sure that if a CO has the same name as a CI, they point directly
+    if ( !Abc_NtkCheckUniqueCioNames(pNtk) )
+        return 0;
+
     return 1;
 }
 
@@ -804,6 +817,121 @@ int Abc_NtkIsAcyclicHierarchy( Abc_Ntk_t * pNtk )
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns 0 if CI names are repeated.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkNamesCompare( char ** pName1, char ** pName2 )
+{
+    return strcmp( *pName1, *pName2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 0 if CI names are repeated.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCheckUniqueCiNames( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNames;
+    Abc_Obj_t * pObj;
+    int i, fRetValue = 1;
+    assert( !Abc_NtkIsNetlist(pNtk) );
+    vNames = Vec_PtrAlloc( Abc_NtkCiNum(pNtk) );
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        Vec_PtrPush( vNames, Abc_ObjName(pObj) );
+    Vec_PtrSort( vNames, Abc_NtkNamesCompare );
+    for ( i = 1; i < Abc_NtkCiNum(pNtk); i++ )
+        if ( !strcmp( Vec_PtrEntry(vNames,i-1), Vec_PtrEntry(vNames,i) ) )
+        {
+            printf( "Abc_NtkCheck: Repeated CI names: %s and %s.\n", Vec_PtrEntry(vNames,i-1), Vec_PtrEntry(vNames,i) );
+            fRetValue = 0;
+        }
+    Vec_PtrFree( vNames );
+    return fRetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 0 if CO names are repeated.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNames;
+    Abc_Obj_t * pObj;
+    int i, fRetValue = 1;
+    assert( !Abc_NtkIsNetlist(pNtk) );
+    vNames = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Vec_PtrPush( vNames, Abc_ObjName(pObj) );
+    Vec_PtrSort( vNames, Abc_NtkNamesCompare );
+    for ( i = 1; i < Abc_NtkCoNum(pNtk); i++ )
+    {
+//        printf( "%s\n", Vec_PtrEntry(vNames,i) );
+        if ( !strcmp( Vec_PtrEntry(vNames,i-1), Vec_PtrEntry(vNames,i) ) )
+        {
+            printf( "Abc_NtkCheck: Repeated CO names: %s and %s.\n", Vec_PtrEntry(vNames,i-1), Vec_PtrEntry(vNames,i) );
+            fRetValue = 0;
+        }
+    }
+    Vec_PtrFree( vNames );
+    return fRetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 0 if there is a pair of CI/CO with the same name and logic in between.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj, * pObjCi;
+    int i, nCiId, fRetValue = 1;
+    assert( !Abc_NtkIsNetlist(pNtk) );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        nCiId = Nm_ManFindIdByName( pNtk->pManName, Abc_ObjName(pObj), ABC_OBJ_PI );
+        if ( nCiId == -1 )
+            nCiId = Nm_ManFindIdByName( pNtk->pManName, Abc_ObjName(pObj), ABC_OBJ_BO );
+        if ( nCiId == -1 )
+            continue;
+        pObjCi = Abc_NtkObj( pNtk, nCiId );
+        assert( !strcmp( Abc_ObjName(pObj), Abc_ObjName(pObjCi) ) );
+        if ( Abc_ObjFanin0(pObj) != pObjCi )
+        {
+            printf( "Abc_NtkCheck: A CI/CO pair share the name (%s) but do not link directly.\n", Abc_ObjName(pObj) );
+            fRetValue = 0;
+        }
+    }
+    return fRetValue;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index da4617ca..3dd9a132 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -884,7 +884,8 @@ int Abc_NtkLevelReverse_rec( Abc_Obj_t * pNode )
         if ( pNode->Level < (unsigned)Level )
             pNode->Level = Level;
     }
-    pNode->Level++;
+    if ( Abc_ObjFaninNum(pNode) > 0 )
+        pNode->Level++;
     return pNode->Level;
 }
 
@@ -975,8 +976,8 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode )
     if ( Abc_NodeIsTravIdCurrent(pNode) )
     {
         fprintf( stdout, "Network \"%s\" contains combinational loop!\n", Abc_NtkName(pNtk) );
-        fprintf( stdout, "Node \"%s\" is encountered twice on the following path:\n", Abc_ObjName(pNode) );
-        fprintf( stdout, " %s", Abc_ObjIsNode(pNode)? Abc_ObjName(pNode) : Abc_NtkName(pNode->pData) );
+        fprintf( stdout, "Node \"%s\" is encountered twice on the following path:\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+        fprintf( stdout, " %s", Abc_ObjIsNode(pNode)? Abc_ObjName(Abc_ObjFanout0(pNode)) : Abc_NtkName(pNode->pData) );
         return 0;
     }
     // mark this node as a node on the current path
@@ -1041,7 +1042,7 @@ bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk )
         if ( fAcyclic = Abc_NtkIsAcyclic_rec(pNode) )
             continue;
         // stop as soon as the first loop is detected
-        fprintf( stdout, " (cone of CO \"%s\")\n", Abc_ObjName(pNode) );
+        fprintf( stdout, " (cone of CO \"%s\")\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
         break;
     }
     return fAcyclic;
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 0947b58a..7a271338 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -880,6 +880,22 @@ int Abc_NtkMapToSop( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Converts SOP functions into BLIF-MV functions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkSopToBlifMv( Abc_Ntk_t * pNtk )
+{
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Convers logic network to the SOP form.]
 
   Description []
diff --git a/src/base/abc/abcHie.c b/src/base/abc/abcHie.c
index b38afb59..9e9d921b 100644
--- a/src/base/abc/abcHie.c
+++ b/src/base/abc/abcHie.c
@@ -146,6 +146,15 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in
         // call recursively
         Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtkModel, pCounter );
     }
+
+    // if it is a BLIF-MV netlist transfer the values of all nets
+    if ( Abc_NtkHasBlifMv(pNtk) && Abc_NtkMvVar(pNtk) )
+    {
+        if ( Abc_NtkMvVar( pNtkNew ) == NULL )
+            Abc_NtkStartMvVars( pNtkNew );
+        Abc_NtkForEachNet( pNtk, pObj, i )
+            Abc_NtkSetMvVarValues( pObj->pCopy, Abc_ObjMvVarNum(pObj) );
+    }
 }
 
 /**Function*************************************************************
@@ -198,12 +207,15 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
     printf( "Hierarchy reader flattened %d instances of logic boxes and left %d black boxes.\n", 
         Counter, Abc_NtkBlackboxNum(pNtkNew) );
 
-    // pass the design
-    assert( Vec_PtrEntry(pNtk->pDesign->vModules, 0) == pNtk );
-    pNtkNew->pDesign = Abc_LibDupBlackboxes( pNtk->pDesign, pNtkNew );
-    // update the pointers
-    Abc_NtkForEachBlackbox( pNtkNew, pTerm, i )
-        pTerm->pData = ((Abc_Ntk_t *)pTerm->pData)->pCopy;
+    if ( pNtk->pDesign )
+    {
+        // pass on the design
+        assert( Vec_PtrEntry(pNtk->pDesign->vTops, 0) == pNtk );
+        pNtkNew->pDesign = Abc_LibDupBlackboxes( pNtk->pDesign, pNtkNew );
+        // update the pointers
+        Abc_NtkForEachBlackbox( pNtkNew, pTerm, i )
+            pTerm->pData = ((Abc_Ntk_t *)pTerm->pData)->pCopy;
+    }
 
     // copy the timing information
 //    Abc_ManTimeDup( pNtk, pNtkNew );
@@ -473,276 +485,6 @@ Abc_Ntk_t * Abc_NtkInsertNewLogic( Abc_Ntk_t * pNtkH, Abc_Ntk_t * pNtkL )
     return pNtkNew;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Assigns name with index.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkConvertAssignName( Abc_Obj_t * pObj, Abc_Obj_t * pNet, int Index )
-{
-    char Suffix[16];
-    assert( Abc_ObjIsTerm(pObj) );
-    assert( Abc_ObjIsNet(pNet) );
-    sprintf( Suffix, "[%d]", Index );
-    Abc_ObjAssignName( pObj, Abc_ObjName(pNet), Suffix );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Strashes the BLIF-MV netlist.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkConvertBlifMv( Abc_Ntk_t * pNtk )
-{
-    char * pSop;
-    Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pBits[16];
-    Abc_Obj_t ** pValues, ** pValuesF;
-    Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObj, * pTemp, * pBit, * pFanin, * pNet;
-    int fUsePositional = 0;
-    int i, k, v, nValues, Val, Index, Len, nBits, Def;
-
-    assert( Abc_NtkIsNetlist(pNtk) );
-    assert( Abc_NtkHasBlifMv(pNtk) );
-
-    // clean the node copy fields
-    Abc_NtkCleanCopy( pNtk );
-
-    // start the network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
-    // duplicate the name and the spec
-    pNtkNew->pName = Extra_UtilStrsav( pNtk->pName );
-//    pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pName );
-
-    // check temporary assumptions
-    Abc_NtkForEachNet( pNtk, pObj, i )
-        assert( Abc_ObjMvVarNum(pObj) < 10 );
-
-    // encode the CI nets
-    if ( fUsePositional )
-    {
-        Abc_NtkForEachCi( pNtk, pObj, i )
-        {
-            pNet = Abc_ObjFanout0(pObj);
-            nValues = Abc_ObjMvVarNum(pNet);
-            pValues = ALLOC( Abc_Obj_t *, nValues );
-            // create PIs for the values
-            for ( v = 0; v < nValues; v++ )
-            {
-                pValues[v] = Abc_NtkCreatePi( pNtkNew );
-                Abc_NtkConvertAssignName( pValues[v], pNet, v );
-            }
-            // save the values in the fanout net
-            pNet->pCopy = (Abc_Obj_t *)pValues;
-        }
-    }
-    else
-    {
-        Abc_NtkForEachCi( pNtk, pObj, i )
-        {
-            pNet = Abc_ObjFanout0(pObj);
-            nValues = Abc_ObjMvVarNum(pNet);
-            pValues = ALLOC( Abc_Obj_t *, nValues );
-            // create PIs for the encoding bits
-            nBits = Extra_Base2Log( nValues );
-            for ( k = 0; k < nBits; k++ )
-            {
-                pBits[k] = Abc_NtkCreatePi( pNtkNew );
-                Abc_NtkConvertAssignName( pBits[k], pNet, k );
-            }
-            // encode the values
-            for ( v = 0; v < nValues; v++ )
-            {
-                pValues[v] = Abc_AigConst1(pNtkNew);
-                for ( k = 0; k < nBits; k++ )
-                {
-                    pBit = Abc_ObjNotCond( pBits[k], (v&(1<<k)) == 0 );
-                    pValues[v] = Abc_AigAnd( pNtkNew->pManFunc, pValues[v], pBit );
-                }
-            }
-            // save the values in the fanout net
-            pNet->pCopy = (Abc_Obj_t *)pValues;
-        }
-    }
-
-    // process nodes in the topological order
-    vNodes = Abc_NtkDfs( pNtk, 0 );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-    {
-        assert( Abc_ObjIsNode(pObj) );
-        pNet = Abc_ObjFanout0(pObj);
-        nValues = Abc_ObjMvVarNum(pNet);
-        pValues = ALLOC( Abc_Obj_t *, nValues );
-        for ( v = 0; v < nValues; v++ )
-            pValues[v] = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
-        // get the BLIF-MV formula
-        pSop = pObj->pData;
-        // skip the value line
-        while ( *pSop++ != '\n' );
-
-        // handle the constant
-        if ( Abc_ObjFaninNum(pObj) == 0 )
-        {
-            Index = *pSop-'0';
-            pValues[Index] = Abc_AigConst1(pNtkNew);
-            // save the values in the fanout net
-            pNet->pCopy = (Abc_Obj_t *)pValues;
-            continue;
-        }
-/*
-        // handle the mux
-        if ( *pSop != 'd' )
-        {
-            assert( Abc_ObjFaninNum(pObj) == 3 );
-            pValuesF = (Abc_Obj_t **)Abc_ObjFanin(pObj,1)->pCopy;
-            for ( v = 0; v < nValues; v++ )
-                pValues[v] = pValuesF[v];
-            // save the values in the fanout net
-            pNet->pCopy = (Abc_Obj_t *)pValues;
-            continue;
-        }
-*/
-        // detect muxes
-        Len = strlen(pSop);
-        for ( k = 0; k < Len; k++ )
-            if ( *(pSop+k) == '=' )
-                break;
-        if ( k < Len )
-        {
-            assert( Abc_ObjFaninNum(pObj) == 3 );
-            pValuesF = (Abc_Obj_t **)Abc_ObjFanin(pObj,1)->pCopy;
-            for ( v = 0; v < nValues; v++ )
-                pValues[v] = pValuesF[v];
-            // save the values in the fanout net
-            pNet->pCopy = (Abc_Obj_t *)pValues;
-            continue;
-        }
- 
-        // skip the default line
-//        assert( *pSop == 'd' );
-        if ( *pSop == 'd' )
-        {
-            Def = *(pSop+1) - '0';
-            while ( *pSop++ != '\n' );
-        }
-        else
-            Def = -1;
-        // convert the values
-        while ( *pSop )
-        {
-            // encode the values
-            pTemp = Abc_AigConst1(pNtkNew); 
-            Abc_ObjForEachFanin( pObj, pFanin, k )
-            {
-                if ( *pSop == '-' )
-                {
-                    pSop += 2;
-                    continue;
-                }
-                Val = Abc_ObjMvVarNum(pFanin);
-                pValuesF = (Abc_Obj_t **)pFanin->pCopy;
-                Index = *pSop-'0';
-                assert( Index >= 0 && Index <= 9 && Index < Val );
-                pTemp = Abc_AigAnd( pNtkNew->pManFunc, pTemp, pValuesF[Index] );
-                pSop += 2;
-            }
-            // get the output value
-            Index = *pSop-'0';
-            assert( Index >= 0 && Index <= 9 );
-            pValues[Index] = Abc_AigOr( pNtkNew->pManFunc, pValues[Index], pTemp );
-            pSop++;
-            assert( *pSop == '\n' );
-            pSop++;
-        }
-        // compute the default value
-//        Def = 0;
-        if ( Def >= 0 )
-        {
-            assert( pValues[Def] == Abc_ObjNot( Abc_AigConst1(pNtkNew) ) );
-            pValues[Def] = Abc_AigConst1(pNtkNew);
-            for ( v = 0; v < nValues; v++ )
-            {
-                if ( v == Def )
-                    continue;
-                pValues[Def] = Abc_AigAnd( pNtkNew->pManFunc, pValues[Def], Abc_ObjNot(pValues[v]) );
-            }
-            // experiment
-    //        if ( nValues > 2 )
-    //            pValues[Def] = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
-        }
-
-        // save the values in the fanout net
-        pNet->pCopy = (Abc_Obj_t *)pValues;
-    }
-    Vec_PtrFree( vNodes );
-
-    // encode the CO nets
-    if ( fUsePositional )
-    {
-        Abc_NtkForEachCo( pNtk, pObj, i )
-        {
-            pNet = Abc_ObjFanin0(pObj);
-            nValues = Abc_ObjMvVarNum(pNet);
-            pValues = (Abc_Obj_t **)pNet->pCopy;
-            for ( v = 0; v < nValues; v++ )
-            {
-                pTemp = Abc_NtkCreatePo( pNtkNew );
-                Abc_ObjAddFanin( pTemp, pValues[v] );
-                Abc_NtkConvertAssignName( pTemp, pNet, v );
-            }
-        }
-    }
-    else
-    {
-        Abc_NtkForEachCo( pNtk, pObj, i )
-        {
-            pNet = Abc_ObjFanin0(pObj);
-            nValues = Abc_ObjMvVarNum(pNet);
-            pValues = (Abc_Obj_t **)pNet->pCopy;
-            nBits = Extra_Base2Log( nValues );
-            for ( k = 0; k < nBits; k++ )
-            {
-                pBit = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
-                for ( v = 0; v < nValues; v++ )
-                    if ( v & (1<<k) )
-                        pBit = Abc_AigOr( pNtkNew->pManFunc, pBit, pValues[v] );
-                pTemp = Abc_NtkCreatePo( pNtkNew );
-                Abc_ObjAddFanin( pTemp, pBit );
-                Abc_NtkConvertAssignName( pTemp, pNet, k );
-            }
-        }
-    }
-
-    // cleanup
-    Abc_NtkForEachObj( pNtk, pObj, i )
-        if ( pObj->pCopy )
-            free( pObj->pCopy );
-
-    Abc_AigCleanup(pNtkNew->pManFunc);
-
-    // check integrity
-    if ( !Abc_NtkCheck( pNtkNew ) )
-    {
-        fprintf( stdout, "Abc_NtkConvertBlifMv(): Network check has failed.\n" );
-        Abc_NtkDelete( pNtkNew );
-        return NULL;
-    }
-    return pNtkNew;
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c
index 1f741ca8..d9d8bce9 100644
--- a/src/base/abc/abcLib.c
+++ b/src/base/abc/abcLib.c
@@ -108,8 +108,11 @@ Abc_Lib_t * Abc_LibDupBlackboxes( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave )
     Abc_Lib_t * pLibNew;
     Abc_Ntk_t * pNtkTemp;
     int i;
+    assert( Vec_PtrSize(pLib->vTops) > 0 );
+    assert( Vec_PtrSize(pLib->vModules) > 1 );
     pLibNew = Abc_LibCreate( pLib->pName );
 //    pLibNew->pManFunc = pNtkSave->pManFunc;
+    Vec_PtrPush( pLibNew->vTops, pNtkSave );
     Vec_PtrPush( pLibNew->vModules, pNtkSave );
     Vec_PtrForEachEntry( pLib->vModules, pNtkTemp, i )
         if ( Abc_NtkHasBlackbox( pNtkTemp ) )
@@ -215,7 +218,50 @@ Abc_Ntk_t * Abc_LibDeriveRoot( Abc_Lib_t * pLib )
     return pNtk;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Detects the top-level models.]
+
+  Description []
+               
+  SideEffects []
 
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_LibFindTopLevelModels( Abc_Lib_t * pLib )
+{
+    Abc_Ntk_t * pNtk, * pNtkBox;
+    Abc_Obj_t * pObj;
+    int i, k;
+    assert( Vec_PtrSize( pLib->vModules ) > 0 );
+    // clear the models
+    Vec_PtrForEachEntry( pLib->vModules, pNtk, i )
+        pNtk->fHieVisited = 0;
+    // mark all the models reachable from other models
+    Vec_PtrForEachEntry( pLib->vModules, pNtk, i )
+    {
+        Abc_NtkForEachBox( pNtk, pObj, k )
+        {
+            if ( Abc_ObjIsLatch(pObj) )
+                continue;
+            if ( pObj->pData == NULL )
+                continue;
+            pNtkBox = pObj->pData;
+            pNtkBox->fHieVisited = 1;
+        }
+    }
+    // collect the models that are not marked
+    Vec_PtrClear( pLib->vTops );
+    Vec_PtrForEachEntry( pLib->vModules, pNtk, i )
+    {
+        if ( pNtk->fHieVisited == 0 )
+            Vec_PtrPush( pLib->vTops, pNtk );
+        else
+            pNtk->fHieVisited = 0;
+    }
+    return Vec_PtrSize( pLib->vTops );
+}
 
 
 /**Function*************************************************************
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index f57bcc21..26b88c68 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -55,7 +55,7 @@ Abc_Ntk_t * Abc_NtkToLogic( Abc_Ntk_t * pNtk )
         return Abc_NtkAigToLogicSop( pNtk );
     assert( Abc_NtkIsNetlist(pNtk) );
     // consider simple case when there is hierarchy
-    assert( pNtk->pDesign == NULL );
+//    assert( pNtk->pDesign == NULL );
     assert( Abc_NtkWhiteboxNum(pNtk) == 0 );
     assert( Abc_NtkBlackboxNum(pNtk) == 0 );
     // start the network
@@ -90,7 +90,7 @@ Abc_Ntk_t * Abc_NtkToLogic( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkToNetlist( Abc_Ntk_t * pNtk, int fDirect )
+Abc_Ntk_t * Abc_NtkToNetlist( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew, * pNtkTemp; 
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) );
@@ -151,6 +151,11 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
     // remove dangling nodes
     Abc_NtkCleanup( pNtk, 0 );
 
+    // make sure the CO names are unique
+    Abc_NtkCheckUniqueCiNames( pNtk );
+    Abc_NtkCheckUniqueCoNames( pNtk );
+    Abc_NtkCheckUniqueCioNames( pNtk );
+
 //    assert( Abc_NtkLogicHasSimpleCos(pNtk) );
     if ( !Abc_NtkLogicHasSimpleCos(pNtk) )
     {
@@ -213,7 +218,7 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
             Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy->pCopy );
     // duplicate EXDC 
     if ( pNtk->pExdc )
-        pNtkNew->pExdc = Abc_NtkToNetlist( pNtk->pExdc, 0 );
+        pNtkNew->pExdc = Abc_NtkToNetlist( pNtk->pExdc );
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkLogicToNetlist(): Network check has failed.\n" );
     return pNtkNew;
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index deddb712..e0773e3f 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -264,18 +264,23 @@ void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsNetlist(pNtk) );
 
     // check if constant 0 net is used
-    pNet = Abc_NtkFindOrCreateNet( pNtk, "1\'b0" );
-    if ( Abc_ObjFanoutNum(pNet) == 0 )
-        Abc_NtkDeleteObj(pNet);
-    else if ( Abc_ObjFaninNum(pNet) == 0 )
-        Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst0(pNtk) );
+    pNet = Abc_NtkFindNet( pNtk, "1\'b0" );
+    if ( pNet )
+    {
+        if ( Abc_ObjFanoutNum(pNet) == 0 )
+            Abc_NtkDeleteObj(pNet);
+        else if ( Abc_ObjFaninNum(pNet) == 0 )
+            Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst0(pNtk) );
+    }
     // check if constant 1 net is used
-    pNet = Abc_NtkFindOrCreateNet( pNtk, "1\'b1" );
-    if ( Abc_ObjFanoutNum(pNet) == 0 )
-        Abc_NtkDeleteObj(pNet);
-    else if ( Abc_ObjFaninNum(pNet) == 0 )
-        Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst1(pNtk) );
-
+    pNet = Abc_NtkFindNet( pNtk, "1\'b1" );
+    if ( pNet )
+    {
+        if ( Abc_ObjFanoutNum(pNet) == 0 )
+            Abc_NtkDeleteObj(pNet);
+        else if ( Abc_ObjFaninNum(pNet) == 0 )
+            Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst1(pNtk) );
+    }
     // fix the net drivers
     Abc_NtkFixNonDrivenNets( pNtk );
 
@@ -872,7 +877,10 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     // free node attributes
     Vec_PtrForEachEntry( pNtk->vAttrs, pAttrMan, i )
         if ( pAttrMan )
+        {
+//printf( "deleting attr\n" );
             Vec_AttFree( pAttrMan, 1 );
+        }
     Vec_PtrFree( pNtk->vAttrs );
     FREE( pNtk->pName );
     FREE( pNtk->pSpec );
@@ -892,16 +900,12 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk )
 { 
-    char Buffer[10];
     Vec_Ptr_t * vNets;
     Abc_Obj_t * pNet, * pNode;
     int i;
 
     if ( Abc_NtkNodeNum(pNtk) == 0 )
-    {
-//        pNtk->ntkFunc = ABC_FUNC_BLACKBOX;
         return;
-    }
 
     // check for non-driven nets
     vNets = Vec_PtrAlloc( 100 );
@@ -910,14 +914,7 @@ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk )
         if ( Abc_ObjFaninNum(pNet) > 0 )
             continue;
         // add the constant 0 driver
-        if ( Abc_NtkHasBlifMv(pNtk) )
-        {
-            pNode = Abc_NtkCreateNode( pNtk );   
-            sprintf( Buffer, "%d\n0\n", Abc_ObjMvVarNum(pNet) );
-            pNode->pData = Abc_SopRegister( pNtk->pManFunc, Buffer );
-        }
-        else
-            pNode = Abc_NtkCreateNodeConst0( pNtk );
+        pNode = Abc_NtkCreateNodeConst0( pNtk );
         // add the fanout net
         Abc_ObjAddFanin( pNet, pNode );
         // add the net to those for which the warning will be printed
@@ -927,7 +924,7 @@ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk )
     // print the warning
     if ( vNets->nSize > 0 )
     {
-        printf( "Constant-0 drivers added to %d non-driven nets in network \"%s\":\n", Vec_PtrSize(vNets), pNtk->pName );
+        printf( "Warning: Constant-0 drivers added to %d non-driven nets in network \"%s\":\n", Vec_PtrSize(vNets), pNtk->pName );
         Vec_PtrForEachEntry( vNets, pNet, i )
         {
             printf( "%s%s", (i? ", ": ""), Abc_ObjName(pNet) );
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 4931f238..0425d984 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -349,7 +349,7 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName
         {
             if ( Abc_NtkIsStrash(pNtkNew) ) 
             {}
-            else if ( Abc_NtkHasSop(pNtkNew) )
+            else if ( Abc_NtkHasSop(pNtkNew) || Abc_NtkHasBlifMv(pNtkNew) )
                 pObjNew->pData = Abc_SopRegister( pNtkNew->pManFunc, pObj->pData );
             else if ( Abc_NtkHasBdd(pNtkNew) )
                 pObjNew->pData = Cudd_bddTransfer(pObj->pNtk->pManFunc, pNtkNew->pManFunc, pObj->pData), Cudd_Ref(pObjNew->pData);
@@ -558,8 +558,9 @@ Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName )
     assert( Abc_NtkIsNetlist(pNtk) );
     if ( pName && (pNet = Abc_NtkFindNet( pNtk, pName )) )
         return pNet;
+//printf( "Creating net %s.\n", pName );
     // create a new net
-    pNet = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET );
+    pNet = Abc_NtkCreateNet( pNtk );
     if ( pName )
         Nm_ManStoreIdName( pNtk->pManName, pNet->Id, pNet->Type, pName, NULL );
     return pNet;
@@ -581,7 +582,7 @@ Abc_Obj_t * Abc_NtkCreateNodeConst0( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pNode;
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) );
     pNode = Abc_NtkCreateNode( pNtk );   
-    if ( Abc_NtkHasSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) || Abc_NtkHasBlifMv(pNtk) )
         pNode->pData = Abc_SopRegister( pNtk->pManFunc, " 0\n" );
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_ReadLogicZero(pNtk->pManFunc), Cudd_Ref( pNode->pData );
@@ -610,7 +611,7 @@ Abc_Obj_t * Abc_NtkCreateNodeConst1( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pNode;
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) );
     pNode = Abc_NtkCreateNode( pNtk );   
-    if ( Abc_NtkHasSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) || Abc_NtkHasBlifMv(pNtk) )
         pNode->pData = Abc_SopRegister( pNtk->pManFunc, " 1\n" );
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_ReadOne(pNtk->pManFunc), Cudd_Ref( pNode->pData );
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index 0836bb89..a39bd7bf 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -933,6 +933,139 @@ char * Abc_SopFromTruthHex( char * pTruth )
     return pSopCover;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Creates one encoder node.]
+
+  Description [Produces MV-SOP for BLIF-MV representation.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopEncoderPos( Extra_MmFlex_t * pMan, int iValue, int nValues )
+{
+    char Buffer[32];
+    assert( iValue < nValues );
+    sprintf( Buffer, "d0\n%d 1\n", iValue );
+    return Abc_SopRegister( pMan, Buffer );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates one encoder node.]
+
+  Description [Produces MV-SOP for BLIF-MV representation.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopEncoderLog( Extra_MmFlex_t * pMan, int iBit, int nValues )
+{
+    char * pResult;
+    Vec_Str_t * vSop;
+    int v, Counter, fFirst = 1, nBits = Extra_Base2Log(nValues);
+    assert( iBit < nBits );
+    // count the number of literals
+    Counter = 0;
+    for ( v = 0; v < nValues; v++ )
+        Counter += ( (v & (1 << iBit)) > 0 );
+    // create the cover
+    vSop = Vec_StrAlloc( 100 );
+    Vec_StrPrintStr( vSop, "d0\n" );
+    if ( Counter > 1 )
+        Vec_StrPrintStr( vSop, "(" );
+    for ( v = 0; v < nValues; v++ )
+        if ( v & (1 << iBit) )
+        {
+            if ( fFirst )
+                fFirst = 0;
+            else
+                Vec_StrPush( vSop, ',' );
+            Vec_StrPrintNum( vSop, v );
+        }
+    if ( Counter > 1 )
+        Vec_StrPrintStr( vSop, ")" );
+    Vec_StrPrintStr( vSop, " 1\n" );
+    Vec_StrPush( vSop, 0 );
+    pResult = Abc_SopRegister( pMan, Vec_StrArray(vSop) );
+    Vec_StrFree( vSop );
+    return pResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the decoder node.]
+
+  Description [Produces MV-SOP for BLIF-MV representation.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopDecoderPos( Extra_MmFlex_t * pMan, int nValues )
+{
+    char * pResult;
+    Vec_Str_t * vSop;
+    int i, k;
+    assert( nValues > 1 );
+    vSop = Vec_StrAlloc( 100 );
+    for ( i = 0; i < nValues; i++ )
+    {
+        for ( k = 0; k < nValues; k++ )
+        {
+            if ( k == i )
+                Vec_StrPrintStr( vSop, "1 " );
+            else
+                Vec_StrPrintStr( vSop, "- " );
+        }
+        Vec_StrPrintNum( vSop, i );
+        Vec_StrPush( vSop, '\n' );
+    }
+    Vec_StrPush( vSop, 0 );
+    pResult = Abc_SopRegister( pMan, Vec_StrArray(vSop) );
+    Vec_StrFree( vSop );
+    return pResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the decover node.]
+
+  Description [Produces MV-SOP for BLIF-MV representation.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopDecoderLog( Extra_MmFlex_t * pMan, int nValues )
+{
+    char * pResult;
+    Vec_Str_t * vSop;
+    int i, b, nBits = Extra_Base2Log(nValues);
+    assert( nValues > 1 && nValues <= (1<<nBits) );
+    vSop = Vec_StrAlloc( 100 );
+    for ( i = 0; i < nValues; i++ )
+    {
+        for ( b = 0; b < nBits; b++ )
+        {
+            Vec_StrPrintNum( vSop, (int)((i & (1 << b)) > 0) );
+            Vec_StrPush( vSop, ' ' );
+        }
+        Vec_StrPrintNum( vSop, i );
+        Vec_StrPush( vSop, '\n' );
+    }
+    Vec_StrPush( vSop, 0 );
+    pResult = Abc_SopRegister( pMan, Vec_StrArray(vSop) );
+    Vec_StrFree( vSop );
+    return pResult;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 353bf046..84952019 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -55,43 +55,6 @@ void * Abc_NtkAttrFree( Abc_Ntk_t * pNtk, int Attr, int fFreeMan )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the Mv-Var manager.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkStartMvVars( Abc_Ntk_t * pNtk ) 
-{
-    Vec_Att_t * pAttMan;
-    assert( Abc_NtkMvVar(pNtk) == NULL );
-    pAttMan = Vec_AttAlloc( 0, Abc_NtkObjNumMax(pNtk) + 1, Extra_MmFlexStart(), Extra_MmFlexStop, NULL, NULL );
-    Vec_PtrWriteEntry( pNtk->vAttrs, VEC_ATTR_MVVAR, pAttMan );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the Mv-Var manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkFreeMvVars( Abc_Ntk_t * pNtk ) 
-{ 
-    void * pUserMan;
-    pUserMan = Abc_NtkAttrFree( pNtk, VEC_ATTR_GLOBAL_BDD, 0 ); 
-    Extra_MmFlexStop( pUserMan );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Increments the current traversal ID of the network.]
 
   Description []
@@ -754,12 +717,6 @@ bool Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk )
     Abc_NtkIncrementTravId( pNtk );
     Abc_NtkForEachCo( pNtk, pNode, i ) 
     {
-/*
-        if ( strcmp( Abc_ObjName(pNode), "g704" ) == 0 )
-        {
-            int s = 1;
-        }
-*/
         // if the driver is complemented, this is an error
         pDriver = Abc_ObjFanin0(pNode);
         if ( Abc_ObjFaninC0(pNode) )
diff --git a/src/base/abc/module.make b/src/base/abc/module.make
index 5edf9000..7b34d8f6 100644
--- a/src/base/abc/module.make
+++ b/src/base/abc/module.make
@@ -1,4 +1,5 @@
 SRC +=    src/base/abc/abcAig.c \
+    src/base/abc/abcBlifMv.c \
     src/base/abc/abcCheck.c \
     src/base/abc/abcDfs.c \
     src/base/abc/abcFanio.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index cf7cc0e9..dc185302 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -46,6 +46,7 @@ static int Abc_CommandPrintAuto      ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandPrintKMap      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintGates     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintSharing   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintXCut      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandShow           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandShowBdd        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -187,6 +188,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Printing",     "print_kmap",    Abc_CommandPrintKMap,        0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_gates",   Abc_CommandPrintGates,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_sharing", Abc_CommandPrintSharing,     0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "print_xcut",    Abc_CommandPrintXCut,        0 );
 
     Cmd_CommandAdd( pAbc, "Printing",     "show",          Abc_CommandShow,             0 );
     Cmd_CommandAdd( pAbc, "Printing",     "show_bdd",      Abc_CommandShowBdd,          0 );
@@ -1405,6 +1407,64 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandPrintXCut( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int fUseLibrary;
+
+    extern int Abc_NtkCrossCut( Abc_Ntk_t * pNtk );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fUseLibrary = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'l':
+            fUseLibrary ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    Abc_NtkCrossCut( pNtk );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: print_xcut [-h]\n" );
+    fprintf( pErr, "\t        prints the size of the cross cut of the current network\n" );
+//    fprintf( pErr, "\t-l    : used library gate names (if mapped) [default = %s]\n", fUseLibrary? "yes": "no" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandShow( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -2057,8 +2117,9 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fUseBdds;
     int fUseSops;
     int fUseCnfs;
+    int fUseMv;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nLutSize, int nCutsMax, int nFlowIters, int nAreaIters, int fArea, int fUseBdds, int fUseSops, int fUseCnfs, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nLutSize, int nCutsMax, int nFlowIters, int nAreaIters, int fArea, int fUseBdds, int fUseSops, int fUseCnfs, int fUseMv, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -2066,16 +2127,17 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nLutSize   =  8;
-    nCutsMax   =  5;
+    nCutsMax   =  4;
     nFlowIters =  1;
     nAreaIters =  1;
     fArea      =  0;
     fUseBdds   =  0;
     fUseSops   =  0;
     fUseCnfs   =  0;
+    fUseMv     =  0;
     fVerbose   =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAabscvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAabscivh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2135,6 +2197,9 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             fUseCnfs ^= 1;
             break;
+        case 'i':
+            fUseMv ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -2145,7 +2210,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
     }
 
-    if ( fUseBdds && fUseSops || fUseBdds && fUseCnfs || fUseSops && fUseCnfs )
+    if ( fUseBdds + fUseSops + fUseCnfs + fUseMv > 1 )
     {
         fprintf( pErr, "Cannot optimize two parameters at the same time.\n" );
         return 1;
@@ -2157,7 +2222,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( nCutsMax < 2 || nCutsMax >= (1<<12) )
+    if ( nCutsMax < 1 || nCutsMax >= (1<<12) )
     {
         fprintf( pErr, "Incorrect number of cuts.\n" );
         return 1;
@@ -2175,7 +2240,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkRenode( pNtk, nLutSize, nCutsMax, nFlowIters, nAreaIters, fArea, fUseBdds, fUseSops, fUseCnfs, fVerbose );
+    pNtkRes = Abc_NtkRenode( pNtk, nLutSize, nCutsMax, nFlowIters, nAreaIters, fArea, fUseBdds, fUseSops, fUseCnfs, fUseMv, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Renoding has failed.\n" );
@@ -2186,16 +2251,17 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: renode [-K num] [-C num] [-F num] [-A num] [-sbcav]\n" );
+    fprintf( pErr, "usage: renode [-K num] [-C num] [-F num] [-A num] [-sbciav]\n" );
     fprintf( pErr, "\t          transforms the AIG into a logic network with larger nodes\n" );
     fprintf( pErr, "\t          while minimizing the number of FF literals of the node SOPs\n" );
     fprintf( pErr, "\t-K num  : the max cut size for renoding (2 < num < %d) [default = %d]\n", IF_MAX_FUNC_LUTSIZE+1, nLutSize );
-    fprintf( pErr, "\t-C num  : the max number of cuts used at a node (1 < num < 2^12) [default = %d]\n", nCutsMax );
+    fprintf( pErr, "\t-C num  : the max number of cuts used at a node (0 < num < 2^12) [default = %d]\n", nCutsMax );
     fprintf( pErr, "\t-F num  : the number of area flow recovery iterations (num >= 0) [default = %d]\n", nFlowIters );
     fprintf( pErr, "\t-A num  : the number of exact area recovery iterations (num >= 0) [default = %d]\n", nAreaIters );
     fprintf( pErr, "\t-s      : toggles minimizing SOP cubes instead of FF lits [default = %s]\n", fUseSops? "yes": "no" );
     fprintf( pErr, "\t-b      : toggles minimizing BDD nodes instead of FF lits [default = %s]\n", fUseBdds? "yes": "no" );
     fprintf( pErr, "\t-c      : toggles minimizing CNF clauses instead of FF lits [default = %s]\n", fUseCnfs? "yes": "no" );
+    fprintf( pErr, "\t-i      : toggles minimizing MV-SOP instead of FF lits [default = %s]\n", fUseMv? "yes": "no" );
     fprintf( pErr, "\t-a      : toggles area-oriented mapping [default = %s]\n", fArea? "yes": "no" );
     fprintf( pErr, "\t-v      : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); 
     fprintf( pErr, "\t-h      : print the command usage\n");
@@ -2706,7 +2772,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     fVeryVerbose = 0;
     fPlaceEnable = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "lxzvwph" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "lxzvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2766,13 +2832,13 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: rewrite [-lzvwph]\n" );
+    fprintf( pErr, "usage: rewrite [-lzvwh]\n" );
     fprintf( pErr, "\t         performs technology-independent rewriting of the AIG\n" );
     fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
     fprintf( pErr, "\t-z     : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w     : toggle printout subgraph statistics [default = %s]\n", fVeryVerbose? "yes": "no" );
-    fprintf( pErr, "\t-p     : toggle placement-aware rewriting [default = %s]\n", fPlaceEnable? "yes": "no" );
+//    fprintf( pErr, "\t-p     : toggle placement-aware rewriting [default = %s]\n", fPlaceEnable? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 } 
@@ -8074,13 +8140,13 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nFlowIters  =  1;
     pPars->nAreaIters  =  2;
     pPars->DelayTarget = -1;
-    pPars->fPreprocess =  1;
+    pPars->fPreprocess =  1;//
     pPars->fArea       =  0;
     pPars->fFancy      =  0;
-    pPars->fExpRed     =  1;
+    pPars->fExpRed     =  1;//
     pPars->fLatchPaths =  0;
     pPars->fSeqMap     =  0;
-    pPars->fVerbose    =  0;
+    pPars->fVerbose    =  0;//
     // internal parameters
     pPars->fTruth      =  0;
     pPars->nLatches    =  pNtk? Abc_NtkLatchNum(pNtk) : 0;
@@ -8206,7 +8272,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( pPars->nCutsMax < 2 || pPars->nCutsMax >= (1<<12) )
+    if ( pPars->nCutsMax < 1 || pPars->nCutsMax >= (1<<12) )
     {
         fprintf( pErr, "Incorrect number of cuts.\n" );
         return 1;
@@ -8279,7 +8345,7 @@ usage:
     fprintf( pErr, "usage: if [-K num] [-C num] [-F num] [-A num] [-D float] [-pafrsvh]\n" );
     fprintf( pErr, "\t           performs FPGA technology mapping of the network\n" );
     fprintf( pErr, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
-    fprintf( pErr, "\t-C num   : the max number of cuts to use (1 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
+    fprintf( pErr, "\t-C num   : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
     fprintf( pErr, "\t-F num   : the number of area flow recovery iterations (num >= 0) [default = %d]\n", pPars->nFlowIters );
     fprintf( pErr, "\t-A num   : the number of exact area recovery iterations (num >= 0) [default = %d]\n", pPars->nAreaIters );
     fprintf( pErr, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer );  
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 887f6cc9..00861e1b 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -125,9 +125,9 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
     pIfMan = If_ManStart( pPars );
 
     // print warning about excessive memory usage
-    if ( 1.0 * Abc_NtkObjNum(pNtk) * pIfMan->nEntrySize / (1<<30) > 0.5 )
-        printf( "Warning: The mapper is about to allocate %.1f Gb for to represent %d cuts per node.\n", 
-            1.0 * Abc_NtkObjNum(pNtk) * pIfMan->nEntrySize / (1<<30), pPars->nCutsMax );
+    if ( 1.0 * Abc_NtkObjNum(pNtk) * pIfMan->nObjBytes / (1<<30) > 1.0 )
+        printf( "Warning: The mapper will allocate %.1f Gb for to represent the subject graph with %d AIG nodes.\n", 
+            1.0 * Abc_NtkObjNum(pNtk) * pIfMan->nObjBytes / (1<<30), Abc_NtkObjNum(pNtk) );
 
     // create PIs and remember them in the old nodes
     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)If_ManConst1( pIfMan );
@@ -184,7 +184,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     Vec_Int_t * vCover;
     int i, nDupGates;
     // create the new network
-    if ( pIfMan->pPars->fUseBdds || pIfMan->pPars->fUseCnfs )
+    if ( pIfMan->pPars->fUseBdds || pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
         pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
     else if ( pIfMan->pPars->fUseSops )
         pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
@@ -214,7 +214,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
         Abc_NtkDeleteObj( pNodeNew );
     // minimize the node
-    if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseBdds )
+    if ( pIfMan->pPars->fUseBdds || pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
         Abc_NtkSweep( pNtkNew, 0 );
     if ( pIfMan->pPars->fUseBdds )
         Abc_NtkBddReorder( pNtkNew, 0 );
@@ -251,7 +251,7 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
     // create a new node 
     pNodeNew = Abc_NtkCreateNode( pNtkNew );
     pCutBest = If_ObjCutBest( pIfObj );
-    if ( pIfMan->pPars->fUseCnfs )
+    if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
     {
         If_CutForEachLeafReverse( pIfMan, pCutBest, pIfLeaf, i )
             Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) );
@@ -269,7 +269,7 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
             // transform truth table into the BDD 
             pNodeNew->pData = Kit_TruthToBdd( pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), 0 );  Cudd_Ref(pNodeNew->pData); 
         }
-        else if ( pIfMan->pPars->fUseCnfs )
+        else if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
         { 
             // transform truth table into the BDD 
             pNodeNew->pData = Kit_TruthToBdd( pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), 1 );  Cudd_Ref(pNodeNew->pData); 
@@ -329,7 +329,7 @@ Hop_Obj_t * Abc_NodeIfToHop_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_
     If_Cut_t * pCut;
     Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
     // get the best cut
-    pCut = If_ObjCutTriv(pIfObj);
+    pCut = If_ObjCutBest(pIfObj);
     // if the cut is visited, return the result
     if ( If_CutData(pCut) )
         return If_CutData(pCut);
@@ -367,14 +367,14 @@ Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t *
     assert( pCut->nLeaves > 1 );
     // set the leaf variables
     If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
-        If_CutSetData( If_ObjCutTriv(pLeaf), Hop_IthVar(pHopMan, i) );
+        If_CutSetData( If_ObjCutBest(pLeaf), Hop_IthVar(pHopMan, i) );
     // recursively compute the function while collecting visited cuts
     Vec_PtrClear( pIfMan->vTemp );
     gFunc = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pIfObj, pIfMan->vTemp ); 
 //    printf( "%d ", Vec_PtrSize(p->vTemp) );
     // clean the cuts
     If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
-        If_CutSetData( If_ObjCutTriv(pLeaf), NULL );
+        If_CutSetData( If_ObjCutBest(pLeaf), NULL );
     Vec_PtrForEachEntry( pIfMan->vTemp, pCut, i )
         If_CutSetData( pCut, NULL );
     return gFunc;
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index af3f55cf..17db7ed9 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -27,14 +27,16 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static int Abc_NtkRenodeEvalAig( If_Cut_t * pCut );
 static int Abc_NtkRenodeEvalBdd( If_Cut_t * pCut );
 static int Abc_NtkRenodeEvalSop( If_Cut_t * pCut );
 static int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut );
-static int Abc_NtkRenodeEvalAig( If_Cut_t * pCut );
+static int Abc_NtkRenodeEvalMv( If_Cut_t * pCut );
 
-static reo_man * s_pReo      = NULL;
-static DdManager * s_pDd     = NULL;
-static Vec_Int_t * s_vMemory = NULL;
+static reo_man * s_pReo       = NULL;
+static DdManager * s_pDd      = NULL;
+static Vec_Int_t * s_vMemory  = NULL;
+static Vec_Int_t * s_vMemory2 = NULL;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -51,7 +53,7 @@ static Vec_Int_t * s_vMemory = NULL;
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nFlowIters, int nAreaIters, int fArea, int fUseBdds, int fUseSops, int fUseCnfs, int fVerbose )
+Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nFlowIters, int nAreaIters, int fArea, int fUseBdds, int fUseSops, int fUseCnfs, int fUseMv, int fVerbose )
 {
     extern Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
     If_Par_t Pars, * pPars = &Pars;
@@ -85,6 +87,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
     pPars->fUseBdds    =  fUseBdds;
     pPars->fUseSops    =  fUseSops;
     pPars->fUseCnfs    =  fUseCnfs;
+    pPars->fUseMv      =  fUseMv;
     if ( fUseBdds )
         pPars->pFuncCost = Abc_NtkRenodeEvalBdd;
     else if ( fUseSops )
@@ -94,6 +97,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
         pPars->fArea = 1;
         pPars->pFuncCost = Abc_NtkRenodeEvalCnf;
     }
+    else if ( fUseMv )
+        pPars->pFuncCost = Abc_NtkRenodeEvalMv;
     else
         pPars->pFuncCost = Abc_NtkRenodeEvalAig;
 
@@ -108,7 +113,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
     else
     {
         assert( s_vMemory == NULL );
-        s_vMemory = Vec_IntAlloc( 1 << 16 );
+        s_vMemory  = Vec_IntAlloc( 1 << 16 );
+        s_vMemory2 = Vec_IntAlloc( 1 << 16 );
     }
 
     // perform mapping/renoding
@@ -125,7 +131,9 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
     else
     {
         Vec_IntFree( s_vMemory );
+        Vec_IntFree( s_vMemory2 );
         s_vMemory = NULL;
+        s_vMemory2 = NULL;
     }
 
     return pNtkNew;
@@ -133,6 +141,35 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
 
 /**Function*************************************************************
 
+  Synopsis    [Computes the cost based on the factored form.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRenodeEvalAig( If_Cut_t * pCut )
+{
+    Kit_Graph_t * pGraph;
+    int i, nNodes;
+    pGraph = Kit_TruthToGraph( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory );
+    if ( pGraph == NULL )
+    {
+        for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
+            pCut->pPerm[i] = 100;
+        return IF_COST_MAX;
+    }
+    nNodes = Kit_GraphNodeNum( pGraph );
+    for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
+        pCut->pPerm[i] = Kit_GraphLeafDepth_rec( pGraph, Kit_GraphNodeLast(pGraph), Kit_GraphNode(pGraph, i) );
+    Kit_GraphFree( pGraph );
+    return nNodes;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes the cost based on the BDD size after reordering.]
 
   Description []
@@ -178,7 +215,7 @@ int Abc_NtkRenodeEvalSop( If_Cut_t * pCut )
         pCut->pPerm[i] = 1;
     RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 1 );
     if ( RetValue == -1 )
-        return ABC_INFINITY;
+        return IF_COST_MAX;
     assert( RetValue == 0 || RetValue == 1 );
     return Vec_IntSize( s_vMemory );
 }
@@ -197,12 +234,13 @@ int Abc_NtkRenodeEvalSop( If_Cut_t * pCut )
 int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut )
 {
     int i, RetValue, nClauses;
+    // set internal mapper parameters
     for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
         pCut->pPerm[i] = 1;
     // compute ISOP for the positive phase
     RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 );
     if ( RetValue == -1 )
-        return ABC_INFINITY;
+        return IF_COST_MAX;
     assert( RetValue == 0 || RetValue == 1 );
     nClauses = Vec_IntSize( s_vMemory );
     // compute ISOP for the negative phase
@@ -210,7 +248,7 @@ int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut )
     RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 );
     Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) );
     if ( RetValue == -1 )
-        return ABC_INFINITY;
+        return IF_COST_MAX;
     assert( RetValue == 0 || RetValue == 1 );
     nClauses += Vec_IntSize( s_vMemory );
     return nClauses;
@@ -218,7 +256,7 @@ int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut )
 
 /**Function*************************************************************
 
-  Synopsis    [Computes the cost based on the factored form.]
+  Synopsis    [Computes the cost of MV-SOP of the cut function.]
 
   Description []
                
@@ -227,22 +265,29 @@ int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRenodeEvalAig( If_Cut_t * pCut )
+int Abc_NtkRenodeEvalMv( If_Cut_t * pCut )
 {
-    Kit_Graph_t * pGraph;
-    int i, nNodes;
-    pGraph = Kit_TruthToGraph( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory );
-    if ( pGraph == NULL )
-    {
-        for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
-            pCut->pPerm[i] = 100;
-        return ABC_INFINITY;
-    }
-    nNodes = Kit_GraphNodeNum( pGraph );
+    int i, RetValue;
+    // set internal mapper parameters
     for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
-        pCut->pPerm[i] = Kit_GraphLeafDepth_rec( pGraph, Kit_GraphNodeLast(pGraph), Kit_GraphNode(pGraph, i) );
-    Kit_GraphFree( pGraph );
-    return nNodes;
+        pCut->pPerm[i] = 1;
+    // compute ISOP for the positive phase
+    RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 );
+    if ( RetValue == -1 )
+        return IF_COST_MAX;
+    assert( RetValue == 0 || RetValue == 1 );
+    // compute ISOP for the negative phase
+    Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) );
+    RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory2, 0 );
+    Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) );
+    if ( RetValue == -1 )
+        return IF_COST_MAX;
+    assert( RetValue == 0 || RetValue == 1 );
+    // return the cost of the cut 
+    RetValue = Abc_NodeEvalMvCost( If_CutLeaveNum(pCut), s_vMemory, s_vMemory2 );
+    if ( RetValue >= IF_COST_MAX )
+        return IF_COST_MAX;
+    return RetValue;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 92691d6c..845f9d77 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -1265,7 +1265,7 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
     }
 
     // write out the current network
-    pNetlist = Abc_NtkToNetlist(pNtk,0);
+    pNetlist = Abc_NtkToNetlist(pNtk);
     if ( pNetlist == NULL )
     {
         fprintf( pErr, "Cannot produce the intermediate network.\n" );
@@ -1406,7 +1406,7 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
     }
 
     // write out the current network
-    pNetlist = Abc_NtkToNetlist(pNtk,0);
+    pNetlist = Abc_NtkToNetlist(pNtk);
     if ( pNetlist == NULL )
     {
         fprintf( pErr, "Cannot produce the intermediate network.\n" );
@@ -1552,7 +1552,7 @@ int CmdCommandCapo( Abc_Frame_t * pAbc, int argc, char **argv )
     }
 
     // write out the current network
-    pNetlist = Abc_NtkToNetlist(pNtk,0);
+    pNetlist = Abc_NtkToNetlist(pNtk);
     if ( pNetlist == NULL )
     {
         fprintf( pErr, "Cannot produce the intermediate network.\n" );
diff --git a/src/base/io/io.h b/src/base/io/io.h
index 472e7b2d..7e23b6e4 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -95,8 +95,7 @@ extern void               Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * pFileName,
 extern void               Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
 extern void               Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk );
 /*=== abcWriteBlifMv.c ==========================================================*/ 
-extern void               Io_WriteBlifMvDesign( Abc_Lib_t * pLib, char * FileName );
-extern void               Io_WriteBlifMvNetlist( Abc_Ntk_t * pNtk, char * FileName );
+extern void               Io_WriteBlifMv( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteBench.c =========================================================*/
 extern int                Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteCnf.c ===========================================================*/
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 3e09caf0..dc72c591 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -62,11 +62,13 @@ struct Io_MvMan_t_
 {
     // general info about file
     int                  fBlifMv;      // the file is BLIF-MV
+    int                  fUseReset;    // the reset circuitry is added
     char *               pFileName;    // the name of the file
     char *               pBuffer;      // the contents of the file
     Vec_Ptr_t *          vLines;       // the line beginnings
     // the results of reading
     Abc_Lib_t *          pDesign;      // the design under construction
+    int                  nNDnodes;     // the counter of ND nodes
     // intermediate storage for models
     Vec_Ptr_t *          vModels;      // vector of models
     Io_MvMod_t *         pLatest;      // the current model
@@ -99,6 +101,7 @@ static int               Io_MvParseLineMv( Io_MvMod_t * p, char * pLine );
 static int               Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset );
 static int               Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine );
 static int               Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens );
+static Io_MvVar_t *      Abc_NtkMvVarDup( Abc_Ntk_t * pNtk, Io_MvVar_t * pVar );
 
 static int               Io_MvCharIsSpace( char s )  { return s == ' ' || s == '\t' || s == '\r' || s == '\n';  }
 static int               Io_MvCharIsMvSymb( char s ) { return s == '(' || s == ')' || s == '{' || s == '}' || s == '-' || s == ',' || s == '!';  }
@@ -127,7 +130,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     Abc_Ntk_t * pNtk;
     Abc_Lib_t * pDesign;
     char * pDesignName;
-    int i;
+    int RetValue, i;
 
     // check that the file is available
     pFile = fopen( pFileName, "rb" );
@@ -141,6 +144,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     // start the file reader
     p = Io_MvAlloc();
     p->fBlifMv   = fBlifMv;
+    p->fUseReset = 0;
     p->pFileName = pFileName;
     p->pBuffer   = Io_MvLoadFile( pFileName );
     if ( p->pBuffer == NULL )
@@ -152,6 +156,9 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     pDesignName  = Extra_FileNameGeneric( pFileName );
     p->pDesign   = Abc_LibCreate( pDesignName );
     free( pDesignName );
+    // free the HOP manager
+    Hop_ManStop( p->pDesign->pManFunc );
+    p->pDesign->pManFunc = NULL;
     // prepare the file for parsing
     Io_MvReadPreparse( p );
     // parse interfaces of each network
@@ -163,6 +170,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     if ( pDesign == NULL )
         return NULL;
     Io_MvFree( p );
+// pDesign should be linked to all models of the design
 
     // make sure that everything is okay with the network structure
     if ( fCheck )
@@ -177,11 +185,19 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
             }
         }
     }
-// pDesign should be linked to all models of the design
+
+//Abc_LibPrint( pDesign );
+
+    // detect top-level model
+    RetValue = Abc_LibFindTopLevelModels( pDesign );
+    pNtk = Vec_PtrEntry( pDesign->vTops, 0 );
+    if ( RetValue > 1 )
+        printf( "Warning: The design has %d root-level modules. The first one (%s) will be used.\n",
+            Vec_PtrSize(pDesign->vTops), pNtk->pName );
 
     // extract the master network
-    pNtk = Vec_PtrEntry( pDesign->vModules, 0 );
     pNtk->pDesign = pDesign;
+    pDesign->pManFunc = NULL;
 
     // verify the design for cyclic dependence
     assert( Vec_PtrSize(pDesign->vModules) > 0 );
@@ -195,10 +211,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     else
         Abc_NtkIsAcyclicHierarchy( pNtk );
 
-//Io_WriteBlifMvDesign( pDesign, "_temp_.mv" );
-//Abc_LibPrint( pDesign );
-//Abc_LibFree( pDesign );
-//return NULL;
+//Io_WriteBlifMv( pNtk, "_temp_.mv" );
     return pNtk;
 }
 
@@ -691,16 +704,18 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
                 return NULL;
             }
             // create binary latch with 1-data and 0-init
-            pMod->pResetLatch = Io_ReadCreateResetLatch( pMod->pNtk, p->fBlifMv );
+            if ( p->fUseReset ) 
+                pMod->pResetLatch = Io_ReadCreateResetLatch( pMod->pNtk, p->fBlifMv );
         }
         // parse the latches
         Vec_PtrForEachEntry( pMod->vLatches, pLine, k )
             if ( !Io_MvParseLineLatch( pMod, pLine ) )
                 return NULL;
         // parse the reset lines
-        Vec_PtrForEachEntry( pMod->vResets, pLine, k )
-            if ( !Io_MvParseLineNamesMv( pMod, pLine, 1 ) )
-                return NULL;
+        if ( p->fUseReset )
+            Vec_PtrForEachEntry( pMod->vResets, pLine, k )
+                if ( !Io_MvParseLineNamesMv( pMod, pLine, 1 ) )
+                    return NULL;
         // parse the nodes
         if ( p->fBlifMv )
         {
@@ -721,6 +736,9 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
         // finalize the network
         Abc_NtkFinalizeRead( pMod->pNtk );
     }
+    if ( p->nNDnodes )
+//        printf( "Warning: The parser added %d PIs to replace non-deterministic nodes.\n", p->nNDnodes );
+        printf( "Warning: The parser added %d constant 0 nodes to replace non-deterministic nodes.\n", p->nNDnodes );
     // return the network
     pDesign = p->pDesign;
     p->pDesign = NULL;
@@ -822,7 +840,7 @@ static int Io_MvParseLineOutputs( Io_MvMod_t * p, char * pLine )
 static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine )
 {
     Vec_Ptr_t * vTokens = p->pMan->vTokens;
-    Abc_Obj_t * pObj, * pMux, * pNet;
+    Abc_Obj_t * pObj, * pNet;
     char * pToken;
     int Init;
     Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
@@ -838,33 +856,35 @@ static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine )
     {
         pObj = Io_ReadCreateLatch( p->pNtk, Vec_PtrEntry(vTokens,1), Vec_PtrEntry(vTokens,2) );
         // get initial value
-        if ( Vec_PtrSize(vTokens) > 3 )
-            Init = atoi( Vec_PtrEntry(vTokens,3) );
+        if ( p->pMan->fBlifMv )
+            Abc_LatchSetInit0( pObj );
         else
-            Init = 2;
-        if ( Init < 0 || Init > 2 )
         {
-            sprintf( p->pMan->sError, "Line %d: Initial state of the latch is incorrect \"%s\".", Io_MvGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,3) );
-            return 0;
+            if ( Vec_PtrSize(vTokens) > 3 )
+                Init = atoi( Vec_PtrEntry(vTokens,3) );
+            else
+                Init = 2;
+            if ( Init < 0 || Init > 2 )
+            {
+                sprintf( p->pMan->sError, "Line %d: Initial state of the latch is incorrect \"%s\".", Io_MvGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,3) );
+                return 0;
+            }
+            if ( Init == 0 )
+                Abc_LatchSetInit0( pObj );
+            else if ( Init == 1 )
+                Abc_LatchSetInit1( pObj );
+            else // if ( Init == 2 )
+                Abc_LatchSetInitDc( pObj );
         }
-        if ( Init == 0 )
-            Abc_LatchSetInit0( pObj );
-        else if ( Init == 1 )
-            Abc_LatchSetInit1( pObj );
-        else // if ( Init == 2 )
-            Abc_LatchSetInitDc( pObj );
     }
     else
     {
-        // get the net corresponding to output of reset latch
-        pNet = Abc_ObjFanout0(Abc_ObjFanout0(p->pResetLatch));
-        assert( Abc_ObjIsNet(pNet) );
-        // create mux
-        pMux = Io_ReadCreateResetMux( p->pNtk, Abc_ObjName(pNet), Vec_PtrEntry(vTokens,1), p->pMan->fBlifMv );
-        // get the net of mux output
-        pNet = Abc_ObjFanout0(pMux);
+        // get the net corresponding to the output of the latch
+        pNet = Abc_NtkFindOrCreateNet( p->pNtk, Vec_PtrEntry(vTokens,2) );
+        // get the net corresponding to the latch output (feeding into reset MUX)
+        pNet = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pNet, "_out") );
         // create latch
-        pObj = Io_ReadCreateLatch( p->pNtk, Abc_ObjName(pNet), Vec_PtrEntry(vTokens,2) );
+        pObj = Io_ReadCreateLatch( p->pNtk, Vec_PtrEntry(vTokens,1), Abc_ObjName(pNet) );
         Abc_LatchSetInit0( pObj );
     }
     return 1;
@@ -1180,7 +1200,7 @@ static char * Io_MvParseTableMv( Io_MvMod_t * p, Abc_Obj_t * pNode, Vec_Ptr_t *
     // prepare the place for the cover
     Vec_StrClear( vFunc );
     // write the number of values
-    Io_MvWriteValues( pNode, vFunc );
+//    Io_MvWriteValues( pNode, vFunc );
     // get the first token
     pFirst = Vec_PtrEntry( vTokens2, 0 );
     if ( pFirst[0] == '.' )
@@ -1217,6 +1237,60 @@ static char * Io_MvParseTableMv( Io_MvMod_t * p, Abc_Obj_t * pNode, Vec_Ptr_t *
 
 /**Function*************************************************************
 
+  Synopsis    [Adds reset circuitry corresponding to latch with pName.]
+
+  Description [Returns the reset node's net.]
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Abc_Obj_t * Io_MvParseAddResetCircuit( Io_MvMod_t * p, char * pName )
+{
+    char Buffer[50];
+    Abc_Obj_t * pNode, * pData0Net, * pData1Net, * pResetLONet, * pOutNet;
+    Io_MvVar_t * pVar;
+    // make sure the reset latch exists
+    assert( p->pResetLatch != NULL );
+    // get the reset net
+    pResetLONet = Abc_ObjFanout0(Abc_ObjFanout0(p->pResetLatch));
+    // get the output net
+    pOutNet = Abc_NtkFindOrCreateNet( p->pNtk, pName );
+    // get the data nets
+    pData0Net = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pOutNet, "_reset") );
+    pData1Net = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pOutNet, "_out") );
+    // duplicate MV variables
+    if ( Abc_NtkMvVar(p->pNtk) )
+    {
+        pVar = Abc_ObjMvVar( pOutNet );
+        Abc_ObjSetMvVar( pData0Net, Abc_NtkMvVarDup(p->pNtk, pVar) );
+        Abc_ObjSetMvVar( pData1Net, Abc_NtkMvVarDup(p->pNtk, pVar) );
+    }
+    // create the node
+    pNode = Abc_NtkCreateNode( p->pNtk );
+    // create the output net
+    Abc_ObjAddFanin( pOutNet, pNode );
+    // create the function
+    if ( p->pMan->fBlifMv )
+    {
+//        Vec_Att_t * p = Abc_NtkMvVar( pNtk );
+        int nValues = Abc_ObjMvVarNum(pOutNet);
+//        sprintf( Buffer, "2 %d %d %d\n1 - - =1\n0 - - =2\n", nValues, nValues, nValues );
+        sprintf( Buffer, "1 - - =1\n0 - - =2\n" );
+        pNode->pData = Abc_SopRegister( p->pNtk->pManFunc, Buffer );
+    }
+    else
+        pNode->pData = Abc_SopCreateMux( p->pNtk->pManFunc );
+    // add nets
+    Abc_ObjAddFanin( pNode, pResetLONet );
+    Abc_ObjAddFanin( pNode, pData1Net );
+    Abc_ObjAddFanin( pNode, pData0Net );
+    return pData0Net;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Parses the nodes line.]
 
   Description []
@@ -1241,19 +1315,15 @@ static int Io_MvParseLineNamesMvOne( Io_MvMod_t * p, Vec_Ptr_t * vTokens, Vec_Pt
             sprintf( p->pMan->sError, "Line %d: Latch with output signal \"%s\" does not exist.", Io_MvGetLine(p->pMan, pName), pName );
             return 0;
         }
+/*
         if ( !Abc_ObjIsBo(Abc_ObjFanin0(pNet)) )
         {
             sprintf( p->pMan->sError, "Line %d: Reset line \"%s\" defines signal that is not a latch output.", Io_MvGetLine(p->pMan, pName), pName );
             return 0;
         }
-        // get the latch input
-        pNode = Abc_ObjFanin0(Abc_ObjFanin0(Abc_ObjFanin0(pNet)));
-        assert( Abc_ObjIsBi(pNode) );
-        // get the MUX feeding into the latch
-        pNode = Abc_ObjFanin0(Abc_ObjFanin0(pNode));
-        assert( Abc_ObjFaninNum(pNode) == 3 );
-        // get the corresponding fanin net
-        pNet = Abc_ObjFanin( pNode, 2 );
+*/
+        // construct the reset circuit and get the reset net feeding into it
+        pNet = Io_MvParseAddResetCircuit( p, pName );
         // create fanins
         pNode = Io_ReadCreateNode( p->pNtk, Abc_ObjName(pNet), (char **)(vTokens->pArray + 1), nInputs );
         assert( nInputs == Vec_PtrSize(vTokens) - 2 );
@@ -1292,6 +1362,7 @@ static int Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset )
 {
     Vec_Ptr_t * vTokens = p->pMan->vTokens;
     Vec_Ptr_t * vTokens2 = p->pMan->vTokens2;
+    Abc_Obj_t * pNet;
     char * pName, * pFirst, * pArrow;
     int nInputs, nOutputs, nLiterals, nLines, i;
     assert( p->pMan->fBlifMv );
@@ -1341,27 +1412,23 @@ static int Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset )
     nLines = nLiterals / (nInputs + nOutputs);
     if ( nInputs == 0 && nLines > 1 )
     {
-        Abc_Obj_t * pNode, * pNet;
         // add the outputs to the PIs
         for ( i = 0; i < nOutputs; i++ )
         {
             pName = Vec_PtrEntry( vTokens, Vec_PtrSize(vTokens) - nOutputs + i );
-            fprintf( stdout, "Io_ReadBlifMv(): Adding PI for internal non-deterministic node \"%s\".\n", pName );
             // get the net corresponding to this node
             pNet = Abc_NtkFindOrCreateNet(p->pNtk, pName);
             if ( fReset )
             {
-                // get the latch input
-                pNode = Abc_ObjFanin0(Abc_ObjFanin0(Abc_ObjFanin0(pNet)));
-                assert( Abc_ObjIsBi(pNode) );
-                // get the MUX feeding into the latch
-                pNode = Abc_ObjFanin0(Abc_ObjFanin0(pNode));
-                assert( Abc_ObjFaninNum(pNode) == 3 );
-                // get the corresponding fanin net
-                pNet = Abc_ObjFanin( pNode, 2 );
+                assert( p->pResetLatch != NULL );
+                // construct the reset circuit and get the reset net feeding into it
+                pNet = Io_MvParseAddResetCircuit( p, pName );
             }
-//            Io_ReadCreatePi( p->pNtk, pName );
-            Abc_ObjAddFanin( pNet, Abc_NtkCreatePi(p->pNtk) );
+            // add the new PI node
+//            Abc_ObjAddFanin( pNet, Abc_NtkCreatePi(p->pNtk) );
+//            fprintf( stdout, "Io_ReadBlifMv(): Adding PI for internal non-deterministic node \"%s\".\n", pName );
+            p->pMan->nNDnodes++;
+            Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst0(p->pNtk) );
         }
         return 1;
     }
@@ -1437,7 +1504,7 @@ static char * Io_MvParseTableBlif( Io_MvMod_t * p, char * pTable, int nFanins )
             sprintf( p->pMan->sError, "Line %d: Output value \"%s\" differs from the value in the first line of the table (%d).", Io_MvGetLine(p->pMan, pProduct), pOutput, Polarity );
             return NULL;
         }
-        // parse one product product
+        // parse one product 
         Vec_StrAppend( vFunc, pProduct );
         Vec_StrPush( vFunc, ' ' );
         Vec_StrPush( vFunc, pOutput[0] );
@@ -1487,6 +1554,40 @@ static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Duplicate the MV variable.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Io_MvVar_t * Abc_NtkMvVarDup( Abc_Ntk_t * pNtk, Io_MvVar_t * pVar )
+{
+    Extra_MmFlex_t * pFlex;
+    Io_MvVar_t * pVarDup;
+    int i;
+    if ( pVar == NULL )
+        return NULL;
+    pFlex = Abc_NtkMvVarMan( pNtk );
+    assert( pFlex != NULL );
+    pVarDup = (Io_MvVar_t *)Extra_MmFlexEntryFetch( pFlex, sizeof(Io_MvVar_t) );
+    pVarDup->nValues = pVar->nValues;
+    pVarDup->pNames = NULL;
+    if ( pVar->pNames == NULL )
+        return pVarDup;
+    pVarDup->pNames = (char **)Extra_MmFlexEntryFetch( pFlex, sizeof(char *) * pVar->nValues );
+    for ( i = 0; i < pVar->nValues; i++ )
+    {
+        pVarDup->pNames[i] = (char *)Extra_MmFlexEntryFetch( pFlex, strlen(pVar->pNames[i]) + 1 );
+        strcpy( pVarDup->pNames[i], pVar->pNames[i] );
+    }
+    return pVarDup;
+}
+
 
 #include "mio.h"
 #include "main.h"
diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c
index 090cf254..c64e330c 100644
--- a/src/base/io/ioReadVerilog.c
+++ b/src/base/io/ioReadVerilog.c
@@ -45,14 +45,21 @@ Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck )
 {
     Abc_Ntk_t * pNtk;
     Abc_Lib_t * pDesign;
+    int RetValue;
 
     // parse the verilog file
     pDesign = Ver_ParseFile( pFileName, NULL, fCheck, 1 );
     if ( pDesign == NULL )
         return NULL;
-/*
+
+    // detect top-level model
+    RetValue = Abc_LibFindTopLevelModels( pDesign );
+    pNtk = Vec_PtrEntry( pDesign->vTops, 0 );
+    if ( RetValue > 1 )
+        printf( "Warning: The design has %d root-level modules. The first one (%s) will be used.\n",
+            Vec_PtrSize(pDesign->vTops), pNtk->pName );
+
     // extract the master network
-    pNtk = Vec_PtrEntryLast( pDesign->vModules );
     pNtk->pDesign = pDesign;
     pDesign->pManFunc = NULL;
 
@@ -67,35 +74,11 @@ Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck )
     }
     else
     {
-        // bring the root model to the beginning
-        for ( i = Vec_PtrSize(pDesign->vModules) - 2; i >= 0; i-- )
-            Vec_PtrWriteEntry(pDesign->vModules, i+1, Vec_PtrEntry(pDesign->vModules, i) );
-        Vec_PtrWriteEntry(pDesign->vModules, 0, pNtk );
         // check that there is no cyclic dependency
         Abc_NtkIsAcyclicHierarchy( pNtk );
     }
-*/
-    // extract the master network
-    pNtk = Vec_PtrEntry( pDesign->vModules, 0 );
-    pNtk->pDesign = pDesign;
-    pDesign->pManFunc = NULL;
 
 //Io_WriteVerilog( pNtk, "_temp.v" );
-
-    // verify the design for cyclic dependence
-    assert( Vec_PtrSize(pDesign->vModules) > 0 );
-    if ( Vec_PtrSize(pDesign->vModules) == 1 )
-    {
-//        printf( "Warning: The design is not hierarchical.\n" );
-        Abc_LibFree( pDesign, pNtk );
-        pNtk->pDesign = NULL;
-        pNtk->pSpec = Extra_UtilStrsav( pFileName );
-    }
-    else
-    {
-        // check that there is no cyclic dependency
-        Abc_NtkIsAcyclicHierarchy( pNtk );
-    }
     return pNtk;
 }
 
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index 0ac3181a..9845fbab 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -173,27 +173,6 @@ Abc_Ntk_t * Io_Read( char * pFileName, Io_FileType_t FileType, int fCheck )
         return NULL;
     if ( !Abc_NtkIsNetlist(pNtk) )
         return pNtk;
-    // consider the case of BLIF-MV
-    if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV )
-    {
-        extern Abc_Ntk_t * Abc_NtkConvertBlifMv( Abc_Ntk_t * pNtk );
-Abc_NtkPrintStats( stdout, pNtk, 0 );
-/*
-{
-    FILE * pFile = fopen( "_temp_.mv", "w" );
-    Io_NtkWriteBlifMv( pFile, pNtk );
-    fclose( pFile );
-}
-*/
-        pNtk = Abc_NtkConvertBlifMv( pTemp = pNtk );
-        Abc_NtkDelete( pTemp );
-        if ( pNtk == NULL )
-        {
-            fprintf( stdout, "Converting BLIF-MV has failed.\n" );
-            return NULL;
-        }
-        return pNtk;
-    }
     // flatten logic hierarchy
     assert( Abc_NtkIsNetlist(pNtk) );
     if ( Abc_NtkWhiteboxNum(pNtk) > 0 )
@@ -218,69 +197,19 @@ Abc_NtkPrintStats( stdout, pNtk, 0 );
             return NULL;
         }
     }
-    // convert the netlist into the logic network
-    pNtk = Abc_NtkToLogic( pTemp = pNtk );
-    Abc_NtkDelete( pTemp );
-    if ( pNtk == NULL )
-    {
-        fprintf( stdout, "Converting netlist to logic network after reading has failed.\n" );
-        return NULL;
-    }
-    return pNtk;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Read the network from a file.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Io_ReadHie( char * pFileName, Io_FileType_t FileType, int fCheck )
-{
-    Abc_Ntk_t * pNtk, * pTemp;
-    // detect the file type
-    if ( Io_ReadFileType(pFileName) == IO_FILE_BLIF )
-        pNtk = Io_ReadBlifMv( pFileName, 0, fCheck );
-//    else if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV )
-//        pNtk = Io_ReadBlifMv( pFileName, 1, fCheck );
-    else if ( Io_ReadFileType(pFileName) == IO_FILE_VERILOG )
-        pNtk = Io_ReadVerilog( pFileName, fCheck );
-    else
-    {
-        printf( "Wrong file type.\n" );
-        return NULL;
-    }
-    if ( pNtk == NULL )
-        return NULL;
-//    printf( "\n" );
-    // flatten logic hierarchy
-    assert( Abc_NtkIsNetlist(pNtk) );
-    if ( Abc_NtkWhiteboxNum(pNtk) > 0 )
-    {
-        pNtk = Abc_NtkFlattenLogicHierarchy( pTemp = pNtk );
-        Abc_NtkDelete( pTemp );
-        if ( pNtk == NULL )
-        {
-            fprintf( stdout, "Flattening logic hierarchy has failed.\n" );
-            return NULL;
-        }
-    }
-    // convert blackboxes
-    if ( Abc_NtkBlackboxNum(pNtk) > 0 )
+    // consider the case of BLIF-MV
+    if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV )
     {
-        printf( "Hierarchy reader converted %d instances of blackboxes.\n", Abc_NtkBlackboxNum(pNtk) );
-        pNtk = Abc_NtkConvertBlackboxes( pTemp = pNtk );
+//Abc_NtkPrintStats( stdout, pNtk, 0 );
+//    Io_WriteBlifMv( pNtk, "_temp_.mv" );
+        pNtk = Abc_NtkStrashBlifMv( pTemp = pNtk );
         Abc_NtkDelete( pTemp );
         if ( pNtk == NULL )
         {
-            fprintf( stdout, "Converting blackboxes has failed.\n" );
+            fprintf( stdout, "Converting BLIF-MV to AIG has failed.\n" );
             return NULL;
         }
+        return pNtk;
     }
     // convert the netlist into the logic network
     pNtk = Abc_NtkToLogic( pTemp = pNtk );
@@ -349,7 +278,13 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
         Io_WriteGml( pNtk, pFileName );
         return;
     }
-
+/*
+    if ( FileType == IO_FILE_BLIFMV )
+    {
+        Io_WriteBlifMv( pNtk, pFileName );
+        return;
+    }
+*/
     // convert logic network into netlist
     if ( FileType == IO_FILE_PLA )
     {
@@ -359,15 +294,17 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
             return;
         }
         if ( Abc_NtkIsComb(pNtk) )
-            pNtkTemp = Abc_NtkToNetlist( pNtk, 1 );
+            pNtkTemp = Abc_NtkToNetlist( pNtk );
         else
         {
             fprintf( stdout, "Latches are writen into the PLA file at PI/PO pairs.\n" );
             pNtkCopy = Abc_NtkDup( pNtk );
             Abc_NtkMakeComb( pNtkCopy );
-            pNtkTemp = Abc_NtkToNetlist( pNtk, 1 );
+            pNtkTemp = Abc_NtkToNetlist( pNtk );
             Abc_NtkDelete( pNtkCopy );
         }
+        if ( !Abc_NtkToSop( pNtk, 1 ) )
+            return;
     }
     else if ( FileType == IO_FILE_BENCH )
     {
@@ -379,7 +316,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
         pNtkTemp = Abc_NtkToNetlistBench( pNtk );
     }
     else
-        pNtkTemp = Abc_NtkToNetlist( pNtk, 0 );
+        pNtkTemp = Abc_NtkToNetlist( pNtk );
 
     if ( pNtkTemp == NULL )
     {
@@ -393,6 +330,12 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
             Abc_NtkToSop( pNtkTemp, 0 );
         Io_WriteBlif( pNtkTemp, pFileName, 1 );
     }
+    else if ( FileType == IO_FILE_BLIFMV )
+    {
+        if ( !Abc_NtkConvertToBlifMv( pNtkTemp ) )
+            return;
+        Io_WriteBlifMv( pNtkTemp, pFileName );
+    }
     else if ( FileType == IO_FILE_BENCH )
         Io_WriteBench( pNtkTemp, pFileName );
     else if ( FileType == IO_FILE_PLA )
@@ -439,6 +382,8 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName )
     assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );
     if ( Io_ReadFileType(pBaseName) == IO_FILE_BLIF )
         pNtkBase = Io_ReadBlifMv( pBaseName, 0, 1 );
+    else if ( Io_ReadFileType(pBaseName) == IO_FILE_BLIFMV )
+        pNtkBase = Io_ReadBlifMv( pBaseName, 1, 1 );
     else if ( Io_ReadFileType(pBaseName) == IO_FILE_VERILOG )
         pNtkBase = Io_ReadVerilog( pBaseName, 1 );
     else 
@@ -446,6 +391,7 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName )
     if ( pNtkBase == NULL )
         return;
 
+    // flatten logic hierarchy if present
     if ( Abc_NtkWhiteboxNum(pNtkBase) > 0 )
     {
         pNtkBase = Abc_NtkFlattenLogicHierarchy( pNtkTemp = pNtkBase );
@@ -455,10 +401,27 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName )
     }
 
     // reintroduce the boxes into the netlist
-    if ( Abc_NtkBlackboxNum(pNtkBase) > 0 )
+    if ( Io_ReadFileType(pBaseName) == IO_FILE_BLIFMV ) 
+    {
+        if ( Abc_NtkBlackboxNum(pNtkBase) > 0 )
+        {
+            printf( "Hierarchy writer does not support BLIF-MV with blackboxes.\n" );
+            Abc_NtkDelete( pNtkBase );
+            return;
+        }
+        // convert the current network to BLIF-MV
+        assert( !Abc_NtkIsNetlist(pNtk) );
+        pNtkResult = Abc_NtkToNetlist( pNtk );
+        if ( !Abc_NtkConvertToBlifMv( pNtkResult ) )
+            return;
+        // reintroduce the network
+        pNtkResult = Abc_NtkInsertBlifMv( pNtkBase, pNtkTemp = pNtkResult );
+        Abc_NtkDelete( pNtkTemp );
+    }
+    else if ( Abc_NtkBlackboxNum(pNtkBase) > 0 )
     {
         // derive the netlist
-        pNtkResult = Abc_NtkToNetlist( pNtk, 0 );
+        pNtkResult = Abc_NtkToNetlist( pNtk );
         pNtkResult = Abc_NtkInsertNewLogic( pNtkBase, pNtkTemp = pNtkResult );
         Abc_NtkDelete( pNtkTemp );
         if ( pNtkResult )
@@ -467,7 +430,7 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName )
     else
     {
         printf( "Warning: The output network does not contain blackboxes.\n" );
-        pNtkResult = Abc_NtkToNetlist( pNtk, 0 );
+        pNtkResult = Abc_NtkToNetlist( pNtk );
     }
     Abc_NtkDelete( pNtkBase );
     if ( pNtkResult == NULL )
@@ -486,6 +449,10 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName )
             Abc_NtkToAig( pNtkResult );
         Io_WriteVerilog( pNtkResult, pFileName );
     }
+    else if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV )
+    {
+        Io_WriteBlifMv( pNtkResult, pFileName );
+    }
     else 
         fprintf( stderr, "Unknown output file format.\n" );
 
@@ -614,61 +581,26 @@ Abc_Obj_t * Io_ReadCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO )
 Abc_Obj_t * Io_ReadCreateResetLatch( Abc_Ntk_t * pNtk, int fBlifMv )
 {
     Abc_Obj_t * pLatch, * pNode;
+    Abc_Obj_t * pNetLI, * pNetLO;
     // create latch with 0 init value
-    pLatch = Io_ReadCreateLatch( pNtk, "_resetLI_", "_resetLO_" );
+//    pLatch = Io_ReadCreateLatch( pNtk, "_resetLI_", "_resetLO_" );
+    pNetLI = Abc_NtkCreateNet( pNtk );
+    pNetLO = Abc_NtkCreateNet( pNtk );
+    Abc_ObjAssignName( pNetLI, Abc_ObjName(pNetLI), NULL );
+    Abc_ObjAssignName( pNetLO, Abc_ObjName(pNetLO), NULL );
+    pLatch = Io_ReadCreateLatch( pNtk, Abc_ObjName(pNetLI), Abc_ObjName(pNetLO) );
+    // set the initial value
     Abc_LatchSetInit0( pLatch );
     // feed the latch with constant1- node
-    pNode = Abc_NtkCreateNode( pNtk );   
-    pNode->pData = Abc_SopRegister( pNtk->pManFunc, "2\n1\n" );
+//    pNode = Abc_NtkCreateNode( pNtk );   
+//    pNode->pData = Abc_SopRegister( pNtk->pManFunc, "2\n1\n" );
+    pNode = Abc_NtkCreateNodeConst1( pNtk );
     Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0(pLatch)), pNode );
     return pLatch;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Create a latch with the given input/output.]
-
-  Description [By default, the latch value is unknown (ABC_INIT_NONE).]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Io_ReadCreateResetMux( Abc_Ntk_t * pNtk, char * pResetLO, char * pDataLI, int fBlifMv )
-{
-    char Buffer[50];
-    Abc_Obj_t * pNode, * pData0Net, * pData1Net, * pResetLONet, * pLINet;
-    // get the reset output net
-    pResetLONet = Abc_NtkFindNet( pNtk, pResetLO );
-    assert( pResetLONet );
-    // get the latch input net
-    pData1Net = Abc_NtkFindOrCreateNet( pNtk, pDataLI );
-    // create Data0 net (coming from reset node)
-    pData0Net = Abc_NtkFindOrCreateNet( pNtk, Abc_ObjNameSuffix(pData1Net, "_reset") );
-    // create the node
-    pNode = Abc_NtkCreateNode( pNtk );
-    if ( fBlifMv )
-    {
-//        Vec_Att_t * p = Abc_NtkMvVar( pNtk );
-        int nValues = Abc_ObjMvVarNum(pData1Net);
-        sprintf( Buffer, "2 %d %d %d\n1 - - =1\n0 - - =2\n", nValues, nValues, nValues );
-        pNode->pData = Abc_SopRegister( pNtk->pManFunc, Buffer );
-    }
-    else
-        pNode->pData = Abc_SopCreateMux( pNtk->pManFunc );
-    // add nets
-    Abc_ObjAddFanin( pNode, pResetLONet );
-    Abc_ObjAddFanin( pNode, pData1Net );
-    Abc_ObjAddFanin( pNode, pData0Net );
-    // create the output net
-    pLINet = Abc_NtkFindOrCreateNet( pNtk, Abc_ObjNameSuffix(pData1Net, "_mux") );
-    Abc_ObjAddFanin( pLINet, pNode );
-    return pNode;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Create node and the net driven by it.]
 
   Description []
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index 3b7d78ca..00768356 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -225,7 +225,7 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName )
     // write the buffer
     fwrite( pBuffer, 1, Pos, pFile );
     free( pBuffer );
-
+/*
     // write the symbol table
     // write PIs
     Abc_NtkForEachPi( pNtk, pObj, i )
@@ -236,7 +236,7 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName )
     // write POs
     Abc_NtkForEachPo( pNtk, pObj, i )
         fprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) );
-
+*/
     // write the comment
     fprintf( pFile, "c\n" );
     fprintf( pFile, "%s\n", pNtk->pName );
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index 417fe2a3..c0c29d65 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -56,7 +56,7 @@ void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
 {
     Abc_Ntk_t * pNtkTemp;
     // derive the netlist
-    pNtkTemp = Abc_NtkToNetlist(pNtk,0);
+    pNtkTemp = Abc_NtkToNetlist(pNtk);
     if ( pNtkTemp == NULL )
     {
         fprintf( stdout, "Writing BLIF has failed.\n" );
@@ -80,6 +80,8 @@ void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
 void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
 {
     FILE * pFile;
+    Abc_Ntk_t * pNtkTemp;
+    int i;
     assert( Abc_NtkIsNetlist(pNtk) );
     // start writing the file
     pFile = fopen( FileName, "w" );
@@ -96,18 +98,6 @@ void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
     // write the hierarchy if present
     if ( Abc_NtkBlackboxNum(pNtk) > 0 )
     {
-        Abc_Ntk_t * pNtkTemp;
-        int i;
-/*
-        Abc_Obj_t * pObj;
-        Abc_NtkForEachBlackbox( pNtk, pObj, i )
-        {
-            pNtkTemp = pObj->pData;
-            assert( pNtkTemp != NULL && Abc_NtkHasBlackbox(pNtkTemp) );
-            fprintf( pFile, "\n\n" );
-            Io_NtkWrite( pFile, pNtkTemp, fWriteLatches );
-        }
-*/
         Vec_PtrForEachEntry( pNtk->pDesign->vModules, pNtkTemp, i )
         {
             if ( pNtkTemp == pNtk )
diff --git a/src/base/io/ioWriteBlifMv.c b/src/base/io/ioWriteBlifMv.c
index 597ca945..775a2e07 100644
--- a/src/base/io/ioWriteBlifMv.c
+++ b/src/base/io/ioWriteBlifMv.c
@@ -26,7 +26,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-void Io_NtkWriteBlifMv( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_NtkWriteBlifMv( FILE * pFile, Abc_Ntk_t * pNtk );
 static void Io_NtkWriteBlifMvOne( FILE * pFile, Abc_Ntk_t * pNtk );
 static void Io_NtkWriteBlifMvPis( FILE * pFile, Abc_Ntk_t * pNtk );
 static void Io_NtkWriteBlifMvPos( FILE * pFile, Abc_Ntk_t * pNtk );
@@ -52,49 +52,34 @@ static void Io_NtkWriteBlifMvValues( FILE * pFile, Abc_Obj_t * pNode );
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteBlifMvDesign( Abc_Lib_t * pLib, char * FileName )
+void Io_WriteBlifMv( Abc_Ntk_t * pNtk, char * FileName )
 {
     FILE * pFile;
-    Abc_Ntk_t * pNtk;
+    Abc_Ntk_t * pNtkTemp;
     int i;
+    assert( Abc_NtkIsNetlist(pNtk) );
+    assert( Abc_NtkHasBlifMv(pNtk) );
     // start writing the file
     pFile = fopen( FileName, "w" );
     if ( pFile == NULL )
     {
-        fprintf( stdout, "Io_WriteBlifMvDesign(): Cannot open the output file.\n" );
-        return;
-    }
-    fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pLib->pName, Extra_TimeStamp() );
-    // write the master network
-    Vec_PtrForEachEntry( pLib->vModules, pNtk, i )
-        Io_NtkWriteBlifMv( pFile, pNtk );
-    fclose( pFile );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Write the network into a BLIF file with the given name.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Io_WriteBlifMvNetlist( Abc_Ntk_t * pNtk, char * FileName )
-{
-    FILE * pFile;
-    // start writing the file
-    pFile = fopen( FileName, "w" );
-    if ( pFile == NULL )
-    {
-        fprintf( stdout, "Io_WriteMvNetlist(): Cannot open the output file.\n" );
+        fprintf( stdout, "Io_WriteBlifMv(): Cannot open the output file.\n" );
         return;
     }
     fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
     // write the master network
     Io_NtkWriteBlifMv( pFile, pNtk );
+    // write the remaining networks
+    if ( pNtk->pDesign )
+    {
+        Vec_PtrForEachEntry( pNtk->pDesign->vModules, pNtkTemp, i )
+        {
+            if ( pNtkTemp == pNtk )
+                continue;
+            fprintf( pFile, "\n\n" );
+            Io_NtkWriteBlifMv( pFile, pNtkTemp );
+        }
+    }
     fclose( pFile );
 }
 
@@ -185,7 +170,7 @@ void Io_NtkWriteBlifMvOne( FILE * pFile, Abc_Ntk_t * pNtk )
             Io_NtkWriteBlifMvLatch( pFile, pLatch );
         fprintf( pFile, "\n" );
     }
-
+/*
     // write the subcircuits
     assert( Abc_NtkWhiteboxNum(pNtk) == 0 );
     if ( Abc_NtkBlackboxNum(pNtk) > 0 )
@@ -195,6 +180,18 @@ void Io_NtkWriteBlifMvOne( FILE * pFile, Abc_Ntk_t * pNtk )
             Io_NtkWriteBlifMvSubckt( pFile, pNode );
         fprintf( pFile, "\n" );
     }
+*/
+    if ( Abc_NtkBlackboxNum(pNtk) > 0 || Abc_NtkWhiteboxNum(pNtk) > 0 )
+    {
+        fprintf( pFile, "\n" );
+        Abc_NtkForEachBox( pNtk, pNode, i )
+        {
+            if ( Abc_ObjIsLatch(pNode) )
+                continue;
+            Io_NtkWriteBlifMvSubckt( pFile, pNode );
+        }
+        fprintf( pFile, "\n" );
+    }
 
     // write each internal node
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
@@ -414,26 +411,32 @@ void Io_NtkWriteBlifMvNode( FILE * pFile, Abc_Obj_t * pNode )
     Abc_Obj_t * pFanin;
     char * pCur;
     int nValues, iFanin, i;
-    fprintf( pFile, "\n" );
+
     // write .mv directives for the fanins
-    pCur = Abc_ObjData(pNode);
+    fprintf( pFile, "\n" );
     Abc_ObjForEachFanin( pNode, pFanin, i )
     {
-        nValues = atoi(pCur);
+//        nValues = atoi(pCur);
+        nValues = Abc_ObjMvVarNum( pFanin );
         if ( nValues > 2 )
             fprintf( pFile, ".mv %s %d\n", Abc_ObjName(pFanin), nValues );
-        while ( *pCur++ != ' ' );
+//        while ( *pCur++ != ' ' );
     }
+
     // write .mv directives for the node
-    nValues = atoi(pCur);
+//    nValues = atoi(pCur);
+    nValues = Abc_ObjMvVarNum( Abc_ObjFanout0(pNode) );
     if ( nValues > 2 )
         fprintf( pFile, ".mv %s %d\n", Abc_ObjName(Abc_ObjFanout0(pNode)), nValues );
-    while ( *pCur++ != '\n' );
+//    while ( *pCur++ != '\n' );
+
     // write the .names line
     fprintf( pFile, ".table" );
     Io_NtkWriteBlifMvNodeFanins( pFile, pNode );
     fprintf( pFile, "\n" );
+
     // write the cubes
+    pCur = Abc_ObjData(pNode);
     if ( *pCur == 'd' )
     {
         fprintf( pFile, ".default " );
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index d8bb1855..8ae3cc42 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -277,6 +277,8 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
         {
             if ( (int)pNode->Level != Level )
                 continue;
+            if ( Abc_ObjFaninNum(pNode) == 0 )
+                continue;
 //            fprintf( pFile, "  Node%d [label = \"%d\"", pNode->Id, pNode->Id );
             if ( Abc_NtkIsStrash(pNtk) )
                 pSopString = "";
@@ -313,7 +315,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
                 // check if the costant node is present
                 if ( Abc_ObjFaninNum(pNode) == 0 && Abc_ObjFanoutNum(pNode) > 0 )
                 {
-                    fprintf( pFile, "  Node%d [label = \"Const1\"", pNode->Id );
+                    fprintf( pFile, "  Node%d [label = \"Const%d\"", pNode->Id, Abc_NtkIsStrash(pNode->pNtk) || Abc_NodeIsConst1(pNode) );
                     fprintf( pFile, ", shape = ellipse" );
                     if ( pNode->fMarkB )
                         fprintf( pFile, ", style = filled" );
diff --git a/src/base/ver/ver.h b/src/base/ver/ver.h
index 0ba081db..cf2b7497 100644
--- a/src/base/ver/ver.h
+++ b/src/base/ver/ver.h
@@ -56,6 +56,7 @@ struct Ver_Man_t_
     ProgressBar *   pProgress;
     // current design
     Abc_Lib_t *     pDesign;
+    st_table *      tName2Suffix;
     // error handling
     FILE *          Output;
     int             fTopLevel;
@@ -67,6 +68,7 @@ struct Ver_Man_t_
     Vec_Int_t *     vStackOp;
 };
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index 6c036288..89f9a689 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -61,18 +61,29 @@ static int  Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateT
 static int  Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate );
 static int  Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox );
 static int  Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox );
-static int  Vec_ParseAttachBoxes( Ver_Man_t * pMan );
+static int  Ver_ParseAttachBoxes( Ver_Man_t * pMan );
 
 static Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName );
 static Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName );
 static Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pNetLI, Abc_Obj_t * pNetLO );
 static Abc_Obj_t * Ver_ParseCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet );
 
+static void Ver_ParseRemoveSuffixTable( Ver_Man_t * pMan );
+
 static inline int Ver_NtkIsDefined( Abc_Ntk_t * pNtkBox )  { assert( pNtkBox->pName );     return Abc_NtkPiNum(pNtkBox) || Abc_NtkPoNum(pNtkBox);  }
 static inline int Ver_ObjIsConnected( Abc_Obj_t * pObj )   { assert( Abc_ObjIsBox(pObj) ); return Abc_ObjFaninNum(pObj) || Abc_ObjFanoutNum(pObj); }
 
+//static inline Abc_Obj_t * Abc_NtkCreateNet( Abc_Ntk_t * pNtk )       { return Abc_NtkCreateObj( pNtk, ABC_OBJ_NET );        }
+
 int glo_fMapped = 0; // this is bad!
 
+typedef struct Ver_Bundle_t_    Ver_Bundle_t;
+struct Ver_Bundle_t_
+{
+    char *          pNameFormal;   // the name of the formal net
+    Vec_Ptr_t *     vNetsActual;   // the vector of actual nets (MSB to LSB)
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -201,7 +212,7 @@ void Ver_ParseInternal( Ver_Man_t * pMan )
     }
 
     // process defined and undefined boxes
-    if ( !Vec_ParseAttachBoxes( pMan ) )
+    if ( !Ver_ParseAttachBoxes( pMan ) )
         return;
 
     // connect the boxes and check
@@ -213,7 +224,7 @@ void Ver_ParseInternal( Ver_Man_t * pMan )
         if ( pMan->fCheck && !Abc_NtkCheckRead( pNtk ) )
         {
             pMan->fTopLevel = 1;
-            sprintf( pMan->sError, "The network check has failed.", pNtk->pName );
+            sprintf( pMan->sError, "The network check has failed for network %s.", pNtk->pName );
             Ver_ParsePrintErrorMessage( pMan );
             return;
         }
@@ -391,7 +402,7 @@ int Ver_ParseModule( Ver_Man_t * pMan )
     // make sure we stopped at the opening paranthesis
     if ( Ver_StreamPopChar(p) != '(' )
     {
-        sprintf( pMan->sError, "Cannot find \"(\" after \"module\".", pNtk->pName );
+        sprintf( pMan->sError, "Cannot find \"(\" after \"module\" in network %s.", pNtk->pName );
         Ver_ParsePrintErrorMessage( pMan );
         return 0;
     }
@@ -406,7 +417,12 @@ int Ver_ParseModule( Ver_Man_t * pMan )
     if ( !Ver_ParseSkipComments( pMan ) )
         return 0;
     Symbol = Ver_StreamPopChar(p);
-    assert( Symbol == ';' );
+    if ( Symbol != ';' )
+    {
+        sprintf( pMan->sError, "Expected closing paranthesis after \"module\"." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
 
     // parse the inputs/outputs/registers/wires/inouts
     while ( 1 )
@@ -508,12 +524,88 @@ int Ver_ParseModule( Ver_Man_t * pMan )
             }
         }
     }
+
+    // remove the table if needed
+    Ver_ParseRemoveSuffixTable( pMan );
     return 1;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Parses one directive.]
+  Synopsis    [Lookups the suffix of the signal of the form [m:n].]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseLookupSuffix( Ver_Man_t * pMan, char * pWord, int * pnMsb, int * pnLsb )
+{
+    unsigned Value;
+    *pnMsb = *pnLsb = -1;
+    if ( pMan->tName2Suffix == NULL )
+        return 1;
+    if ( !st_lookup( pMan->tName2Suffix, (char *)pWord, (char **)&Value ) )
+        return 1;
+    *pnMsb = (Value >> 8) & 0xff;
+    *pnLsb = Value & 0xff;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Lookups the suffix of the signal of the form [m:n].]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseInsertsSuffix( Ver_Man_t * pMan, char * pWord, int nMsb, int nLsb )
+{
+    unsigned Value;
+    if ( pMan->tName2Suffix == NULL )
+        pMan->tName2Suffix = st_init_table( strcmp, st_strhash );
+    if ( st_is_member( pMan->tName2Suffix, pWord ) )
+        return 1;
+    assert( nMsb >= 0 && nMsb < 128 );
+    assert( nLsb >= 0 && nLsb < 128 );
+    Value = (nMsb << 8) | nLsb;
+    st_insert( pMan->tName2Suffix, Extra_UtilStrsav(pWord), (char *)Value );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Lookups the suffic of the signal of the form [m:n].]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_ParseRemoveSuffixTable( Ver_Man_t * pMan )
+{
+    st_generator * gen;
+    char * pKey, * pValue;
+    if ( pMan->tName2Suffix == NULL )
+        return;
+    st_foreach_item( pMan->tName2Suffix, gen, (char **)&pKey, (char **)&pValue )
+        free( pKey );
+    st_free_table( pMan->tName2Suffix );
+    pMan->tName2Suffix = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Determine signal prefix of the form [Beg:End].]
 
   Description []
                
@@ -522,16 +614,172 @@ int Ver_ParseModule( Ver_Man_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
+int Ver_ParseSignalPrefix( Ver_Man_t * pMan, char ** ppWord, int * pnMsb, int * pnLsb )
+{
+    char * pWord = *ppWord;
+    int nMsb, nLsb;
+    assert( pWord[0] == '[' );
+    // get the beginning
+    nMsb = atoi( pWord + 1 );
+    // find the splitter
+    while ( *pWord && *pWord != ':' && *pWord != ']' )
+        pWord++;
+    if ( *pWord == 0 )
+    {
+        sprintf( pMan->sError, "Cannot find closing bracket in this line." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    if ( *pWord == ']' )
+        nLsb = nMsb;
+    else
+    {
+        assert( *pWord == ':' );
+        nLsb = atoi( pWord + 1 );
+        // find the closing paranthesis
+        while ( *pWord && *pWord != ']' )
+            pWord++;
+        if ( *pWord == 0 )
+        {
+            sprintf( pMan->sError, "Cannot find closing bracket in this line." );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        assert( *pWord == ']' );
+        pWord++;
+    }
+    assert( nMsb >= 0 && nLsb >= 0 );
+    // return
+    *ppWord = pWord;
+    *pnMsb = nMsb;
+    *pnLsb = nLsb;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Determine signal suffix of the form [m:n].]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseSignalSuffix( Ver_Man_t * pMan, char * pWord, int * pnMsb, int * pnLsb )
+{
+    char * pCur;
+    int Length;
+    Length = strlen(pWord);
+    assert( pWord[Length-1] == ']' );
+    // walk backward
+    for ( pCur = pWord + Length - 2; pCur != pWord; pCur-- )
+        if ( *pCur == ':' || *pCur == '[' )
+            break;
+    if ( pCur == pWord )
+    {
+        sprintf( pMan->sError, "Cannot find opening bracket in signal name %s.", pWord );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    if ( *pCur == '[' )
+    {
+        *pnMsb = *pnLsb = atoi(pCur+1);
+        *pCur = 0;
+        return 1;
+    }
+    assert( *pCur == ':' );
+    // get the end of the interval
+    *pnLsb = atoi(pCur+1);
+    // find the beginning
+    for ( pCur = pWord + Length - 2; pCur != pWord; pCur-- )
+        if ( *pCur == '[' )
+            break;
+    if ( pCur == pWord )
+    {
+        sprintf( pMan->sError, "Cannot find opening bracket in signal name %s.", pWord );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    assert( *pCur == '[' );
+    // get the beginning of the interval
+    *pnMsb = atoi(pCur+1);
+    // cut the word
+    *pCur = 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the values of constant bits.]
+
+  Description [The resulting bits are in MSB to LSB order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseConstant( Ver_Man_t * pMan, char * pWord )
+{
+    int nBits, i;
+    assert( pWord[0] >= '1' && pWord[1] <= '9' );
+    nBits = atoi(pWord);
+    // find the next symbol \'
+    while ( *pWord && *pWord != '\'' )
+        pWord++;
+    if ( *pWord == 0 )
+    {
+        sprintf( pMan->sError, "Cannot find symbol \' in the constant." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    assert( *pWord == '\'' );
+    pWord++;
+    if ( *pWord != 'b' )
+    {
+        sprintf( pMan->sError, "Currently can only handle binary constants." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    pWord++;
+    // scan the bits
+    Vec_PtrClear( pMan->vNames );
+    for ( i = 0; i < nBits; i++ )
+    {
+        if ( pWord[i] != '0' && pWord[i] != '1' )
+        {
+            sprintf( pMan->sError, "Having problem parsing the binary constant." );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        Vec_PtrPush( pMan->vNames, (void *)(pWord[i]-'0') );
+    }
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description [The signals are added in the order from LSB to MSB.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Ver_ParseSignal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_SignalType_t SigType )
 {
     Ver_Stream_t * p = pMan->pReader;
-    char Buffer[1000];
-    int Lower, Upper, i;
-    char * pWord;
-    char Symbol;
-    Lower = Upper = 0;
+    char Buffer[1000], Symbol, * pWord;
+    int nMsb, nLsb, Bit, Limit, i;
+    nMsb = nLsb = -1;
     while ( 1 )
     {
+        // get the next word
         pWord = Ver_ParseGetName( pMan );
         if ( pWord == NULL )
             return 0;
@@ -539,39 +787,11 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_SignalType_t SigTyp
         // check if the range is specified
         if ( pWord[0] == '[' && !pMan->fNameLast )
         {
-            Lower = atoi( pWord + 1 );
-            // find the splitter
-            while ( *pWord && *pWord != ':' && *pWord != ']' )
-                pWord++;
+            assert( nMsb == -1 && nLsb == -1 );
+            Ver_ParseSignalPrefix( pMan, &pWord, &nMsb, &nLsb );
+            // check the case when there is space between bracket and the next word
             if ( *pWord == 0 )
             {
-                sprintf( pMan->sError, "Cannot find closing bracket in this line." );
-                Ver_ParsePrintErrorMessage( pMan );
-                return 0;
-            }
-            if ( *pWord == ']' )
-                Upper = Lower;
-            else
-            {
-                Upper = atoi( pWord + 1 );
-                if ( Lower > Upper )
-                    i = Lower, Lower = Upper, Upper = i;
-                // find the closing paranthesis
-                while ( *pWord && *pWord != ']' )
-                    pWord++;
-                if ( *pWord == 0 )
-                {
-                    sprintf( pMan->sError, "Cannot find closing bracket in this line." );
-                    Ver_ParsePrintErrorMessage( pMan );
-                    return 0;
-                }
-                assert( *pWord == ']' );
-            }
-            // check the case of no space between bracket and the next word
-            if ( *(pWord+1) != 0 )
-                pWord++;
-            else
-            {
                 // get the signal name
                 pWord = Ver_ParseGetName( pMan );
                 if ( pWord == NULL )
@@ -580,7 +800,7 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_SignalType_t SigTyp
         }
 
         // create signals
-        if ( Lower == 0 && Upper == 0 )
+        if ( nMsb == -1 && nLsb == -1 )
         {
             if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT )
                 Ver_ParseCreatePi( pNtk, pWord );
@@ -591,9 +811,14 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_SignalType_t SigTyp
         }
         else
         {
-            for ( i = Lower; i <= Upper; i++ )
+            assert( nMsb >= 0 && nLsb >= 0 );
+            // add to the hash table
+            Ver_ParseInsertsSuffix( pMan, pWord, nMsb, nLsb );
+            // add signals from Lsb to Msb
+            Limit = nMsb > nLsb? nMsb - nLsb + 1: nLsb - nMsb + 1;
+            for ( i = 0, Bit = nLsb; i < Limit; i++, Bit = nMsb > nLsb ? Bit + 1: Bit - 1  )
             {
-                sprintf( Buffer, "%s[%d]", pWord, i );
+                sprintf( Buffer, "%s[%d]", pWord, Bit );
                 if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT )
                     Ver_ParseCreatePi( pNtk, Buffer );
                 if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT )
@@ -823,12 +1048,14 @@ int Ver_ParseInitial( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
 ***********************************************************************/
 int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
 {
+    char Buffer[1000], Buffer2[1000];
     Ver_Stream_t * p = pMan->pReader;
     Abc_Obj_t * pNode, * pNet;
     char * pWord, * pName, * pEquation;
     Hop_Obj_t * pFunc;
     char Symbol;
-    int i, Length, fReduction;
+    int i, Bit, Limit, Length, fReduction;
+    int nMsb, nLsb;
 
 //    if ( Ver_StreamGetLineNumber(p) == 2756 )
 //    {
@@ -845,102 +1072,171 @@ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
         pWord = Ver_ParseGetName( pMan );
         if ( pWord == NULL )
             return 0;
-        // consider the case of reduction operations
-        fReduction = 0;
-        if ( pWord[0] == '{' && !pMan->fNameLast )
-            fReduction = 1;
-        if ( fReduction )
-        {
-            pWord++;
-            pWord[strlen(pWord)-1] = 0;
-            assert( pWord[0] != '\\' );
-        }
-        // get the fanout net
-        pNet = Ver_ParseFindNet( pNtk, pWord );
-        if ( pNet == NULL )
-        {
-            sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
-            Ver_ParsePrintErrorMessage( pMan );
-            return 0;
-        }
-        // get the equality sign
-        if ( Ver_StreamPopChar(p) != '=' )
-        {
-            sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
-            Ver_ParsePrintErrorMessage( pMan );
-            return 0;
-        }
-        // skip the comments
-        if ( !Ver_ParseSkipComments( pMan ) )
+        // check for vector-inputs
+        if ( !Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb ) )
             return 0;
-        // get the second name
-        if ( fReduction )
-            pEquation = Ver_StreamGetWord( p, ";" );
-        else
-            pEquation = Ver_StreamGetWord( p, ",;" );
-        if ( pEquation == NULL )
+        // handle special case of constant assignment
+        if ( nMsb >= 0 && nLsb >= 0 )
         {
-            sprintf( pMan->sError, "Cannot read the equation for %s.", Abc_ObjName(pNet) );
-            Ver_ParsePrintErrorMessage( pMan );
-            return 0;
-        }
+            // save the fanout name
+            strcpy( Buffer, pWord );
+            // get the equality sign
+            if ( Ver_StreamPopChar(p) != '=' )
+            {
+                sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+            // get the constant
+            pWord = Ver_ParseGetName( pMan );
+            if ( pWord == NULL )
+                return 0;
+            // check if it is indeed a constant
+            if ( !(pWord[0] >= '0' && pWord[0] <= '9') )
+            {
+                sprintf( pMan->sError, "Currently can only assign vector-signal \"%s\" to be a constant.", Buffer );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
 
-        // consider the case of mapped network
-        if ( pMan->fMapped )
-        {
-            Vec_PtrClear( pMan->vNames );
-            if ( !strcmp( pEquation, "1\'b0" ) )
-                pFunc = (Hop_Obj_t *)Mio_LibraryReadConst0(Abc_FrameReadLibGen());
-            else if ( !strcmp( pEquation, "1\'b1" ) )
-                pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1(Abc_FrameReadLibGen());
-            else
+            // set individual bits of the constant
+            if ( !Ver_ParseConstant( pMan, pWord ) )
+                return 0;
+            // check that the constant has the same size
+            Limit = nMsb > nLsb? nMsb - nLsb + 1: nLsb - nMsb + 1;
+            if ( Limit != Vec_PtrSize(pMan->vNames) )
+            {
+                sprintf( pMan->sError, "The constant size (%d) is different from the signal\"%s\" size (%d).", 
+                    Vec_PtrSize(pMan->vNames), Buffer, Limit );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+            // iterate through the bits
+            for ( i = 0, Bit = nLsb; i < Limit; i++, Bit = nMsb > nLsb ? Bit + 1: Bit - 1  )
             {
-                if ( Ver_ParseFindNet(pNtk, pEquation) == NULL )
+                // get the fanin net
+                if ( Vec_PtrEntry( pMan->vNames, Limit-1-i ) )
+                    pNet = Ver_ParseFindNet( pNtk, "1\'b1" );
+                else
+                    pNet = Ver_ParseFindNet( pNtk, "1\'b0" );
+                assert( pNet != NULL );
+
+                // create the buffer
+                pNode = Abc_NtkCreateNodeBuf( pNtk, pNet );
+
+                // get the fanout net
+                sprintf( Buffer2, "%s[%d]", Buffer, Bit );
+                pNet = Ver_ParseFindNet( pNtk, Buffer2 );
+                if ( pNet == NULL )
                 {
-                    sprintf( pMan->sError, "Cannot read Verilog with non-trivail assignments in the mapped netlist.", pEquation );
+                    sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
                     Ver_ParsePrintErrorMessage( pMan );
                     return 0;
                 }
-                Vec_PtrPush( pMan->vNames, (void *)strlen(pEquation) );
-                Vec_PtrPush( pMan->vNames, pEquation );
-                // get the buffer
-                pFunc = (Hop_Obj_t *)Mio_LibraryReadBuf(Abc_FrameReadLibGen());
+                Abc_ObjAddFanin( pNet, pNode );
             }
+            // go to the end of the line
+            Ver_ParseSkipComments( pMan );
         }
         else
         {
-            // parse the formula
+            // consider the case of reduction operations
+            fReduction = 0;
+            if ( pWord[0] == '{' && !pMan->fNameLast )
+                fReduction = 1;
             if ( fReduction )
-                pFunc = Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError );  
-            else
-                pFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError );  
-            if ( pFunc == NULL )
             {
+                pWord++;
+                pWord[strlen(pWord)-1] = 0;
+                assert( pWord[0] != '\\' );
+            }
+            // get the fanout net
+            pNet = Ver_ParseFindNet( pNtk, pWord );
+            if ( pNet == NULL )
+            {
+                sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
                 Ver_ParsePrintErrorMessage( pMan );
                 return 0;
             }
-        }
-
-        // create the node with the given inputs
-        pNode = Abc_NtkCreateNode( pNtk );
-        pNode->pData = pFunc;
-        Abc_ObjAddFanin( pNet, pNode );
-        // connect to fanin nets
-        for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ )
-        {
-            // get the name of this signal
-            Length = (int)Vec_PtrEntry( pMan->vNames, 2*i );
-            pName  = Vec_PtrEntry( pMan->vNames, 2*i + 1 );
-            pName[Length] = 0;
-            // find the corresponding net
-            pNet = Ver_ParseFindNet( pNtk, pName );
-            if ( pNet == NULL )
+            // get the equality sign
+            if ( Ver_StreamPopChar(p) != '=' )
             {
-                sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %d is not defined).", pWord, pName );
+                sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
                 Ver_ParsePrintErrorMessage( pMan );
                 return 0;
             }
-            Abc_ObjAddFanin( pNode, pNet );
+            // skip the comments
+            if ( !Ver_ParseSkipComments( pMan ) )
+                return 0;
+            // get the second name
+            if ( fReduction )
+                pEquation = Ver_StreamGetWord( p, ";" );
+            else
+                pEquation = Ver_StreamGetWord( p, ",;" );
+            if ( pEquation == NULL )
+            {
+                sprintf( pMan->sError, "Cannot read the equation for %s.", Abc_ObjName(pNet) );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+
+            // consider the case of mapped network
+            if ( pMan->fMapped )
+            {
+                Vec_PtrClear( pMan->vNames );
+                if ( !strcmp( pEquation, "1\'b0" ) )
+                    pFunc = (Hop_Obj_t *)Mio_LibraryReadConst0(Abc_FrameReadLibGen());
+                else if ( !strcmp( pEquation, "1\'b1" ) )
+                    pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1(Abc_FrameReadLibGen());
+                else
+                {
+                    if ( Ver_ParseFindNet(pNtk, pEquation) == NULL )
+                    {
+                        sprintf( pMan->sError, "Cannot read Verilog with non-trivial assignments in the mapped netlist." );
+                        Ver_ParsePrintErrorMessage( pMan );
+                        return 0;
+                    }
+                    Vec_PtrPush( pMan->vNames, (void *)strlen(pEquation) );
+                    Vec_PtrPush( pMan->vNames, pEquation );
+                    // get the buffer
+                    pFunc = (Hop_Obj_t *)Mio_LibraryReadBuf(Abc_FrameReadLibGen());
+                }
+            }
+            else
+            {
+                // parse the formula
+                if ( fReduction )
+                    pFunc = Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError );  
+                else
+                    pFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError );  
+                if ( pFunc == NULL )
+                {
+                    Ver_ParsePrintErrorMessage( pMan );
+                    return 0;
+                }
+            }
+
+            // create the node with the given inputs
+            pNode = Abc_NtkCreateNode( pNtk );
+            pNode->pData = pFunc;
+            Abc_ObjAddFanin( pNet, pNode );
+            // connect to fanin nets
+            for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ )
+            {
+                // get the name of this signal
+                Length = (int)Vec_PtrEntry( pMan->vNames, 2*i );
+                pName  = Vec_PtrEntry( pMan->vNames, 2*i + 1 );
+                pName[Length] = 0;
+                // find the corresponding net
+                pNet = Ver_ParseFindNet( pNtk, pName );
+                if ( pNet == NULL )
+                {
+                    sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %s is not defined).", pWord, pName );
+                    Ver_ParsePrintErrorMessage( pMan );
+                    return 0;
+                }
+                Abc_ObjAddFanin( pNode, pNet );
+            }
         }
 
         Symbol = Ver_StreamPopChar(p);
@@ -1229,19 +1525,21 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
 ***********************************************************************/
 int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
 {
+    char Buffer[1000];
     Ver_Stream_t * p = pMan->pReader;
-    Vec_Ptr_t * vNetPairs;
-    Abc_Obj_t * pNetFormal, * pNetActual;
+    Ver_Bundle_t * pBundle;
+    Vec_Ptr_t * vBundles;
+    Abc_Obj_t * pNetActual; 
     Abc_Obj_t * pNode;
     char * pWord, Symbol;
-    int fCompl;
+    int fCompl, fFormalIsGiven;
 
-    // parse the directive and set the pointers to the PIs/POs of the gate
+    // gate the name of the box
     pWord = Ver_ParseGetName( pMan );
     if ( pWord == NULL )
         return 0;
 
-    // create box to represent this gate
+    // create a box with this name
     pNode = Abc_NtkCreateBlackbox( pNtk );
     pNode->pData = pNtkBox;
     Abc_ObjAssignName( pNode, pWord, NULL );
@@ -1253,50 +1551,174 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
         Ver_ParsePrintErrorMessage( pMan );
         return 0;
     }
-
+    Ver_ParseSkipComments( pMan );
+ 
     // parse pairs of formal/actural inputs
-    vNetPairs = Vec_PtrAlloc( 16 );
-    pNode->pCopy = (Abc_Obj_t *)vNetPairs;
+    vBundles = Vec_PtrAlloc( 16 );
+    pNode->pCopy = (Abc_Obj_t *)vBundles;
     while ( 1 )
     {
+        // allocate the bundle (formal name + array of actual nets)
+        pBundle = ALLOC( Ver_Bundle_t, 1 );
+        pBundle->pNameFormal = NULL;
+        pBundle->vNetsActual = Vec_PtrAlloc( 4 );
+        Vec_PtrPush( vBundles, pBundle );
+
         // process one pair of formal/actual parameters
-        if ( Ver_StreamPopChar(p) != '.' )
+        fFormalIsGiven = 0;
+        if ( Ver_StreamScanChar(p) == '.' )
         {
-            sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Abc_ObjName(pNode) );
-            Ver_ParsePrintErrorMessage( pMan );
-            return 0;
-        }
+            fFormalIsGiven = 1;
+            if ( Ver_StreamPopChar(p) != '.' )
+            {
+                sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Abc_ObjName(pNode) );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
 
-        // parse the formal name
-        pWord = Ver_ParseGetName( pMan );
-        if ( pWord == NULL )
-            return 0;
-        // get the formal net
-        pNetFormal = Abc_NtkFindOrCreateNet( pNtkBox, pWord );
-        Vec_PtrPush( vNetPairs, pNetFormal );
+            // parse the formal name
+            pWord = Ver_ParseGetName( pMan );
+            if ( pWord == NULL )
+                return 0;
 
-        // open the paranthesis
-        if ( Ver_StreamPopChar(p) != '(' )
-        {
-            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, Abc_ObjName(pNode));
-            Ver_ParsePrintErrorMessage( pMan );
-            return 0;
+            // save the name
+            pBundle->pNameFormal = Extra_UtilStrsav( pWord );
+
+            // open the paranthesis
+            if ( Ver_StreamPopChar(p) != '(' )
+            {
+                sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, Abc_ObjName(pNode));
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+            Ver_ParseSkipComments( pMan );
         }
 
-        // parse the actual name
-        pWord = Ver_ParseGetName( pMan );
-        if ( pWord == NULL )
-            return 0;
-        // consider the case of empty name
-        fCompl = 0;
-        if ( pWord[0] == 0 )
+        // check if this is the beginning of {} expression
+        Symbol = Ver_StreamScanChar(p);
+
+        // consider the case of vector-inputs
+        if ( Symbol == '{' )
         {
-            // remove the formal net
-//            Vec_PtrPop( vNetPairs );
-            pNetActual = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET );
+            int i, k, Bit, Limit, nMsb, nLsb, fQuit;
+
+            // skip this char
+            Ver_ParseSkipComments( pMan );
+            Ver_StreamPopChar(p);
+
+            // read actual names
+            i = 0;
+            fQuit = 0;
+            while ( 1 )
+            {
+                // parse the formal name
+                Ver_ParseSkipComments( pMan );
+                pWord = Ver_ParseGetName( pMan );
+                if ( pWord == NULL )
+                    return 0;
+
+                // check if the last char is a closing brace
+                if ( pWord[strlen(pWord)-1] == '}' )
+                {
+                    pWord[strlen(pWord)-1] = 0;
+                    fQuit = 1;
+                }
+                if ( pWord[0] == 0 )
+                    break;
+
+                // check for constant
+                if ( pWord[0] >= '1' && pWord[0] <= '9' )
+                {
+                    if ( !Ver_ParseConstant( pMan, pWord ) )
+                        return 0;
+                    // add constant MSB to LSB
+                    for ( k = 0; k < Vec_PtrSize(pMan->vNames); k++, i++ )
+                    {
+                        // get the actual net
+                        sprintf( Buffer, "1\'b%d", (int)(Vec_PtrEntry(pMan->vNames,k) != NULL) );
+                        pNetActual = Ver_ParseFindNet( pNtk, Buffer );
+                        if ( pNetActual == NULL )
+                        {
+                            sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", Buffer, Abc_ObjName(pNode) );
+                            Ver_ParsePrintErrorMessage( pMan );
+                            return 0;
+                        }
+                        Vec_PtrPush( pBundle->vNetsActual, pNetActual );
+                    }
+                }
+                else
+                {
+                    // get the suffix of the form [m:n]
+                    if ( pWord[strlen(pWord)-1] == ']' && !pMan->fNameLast )
+                        Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb );
+                    else
+                        Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb );
+
+                    // generate signals
+                    if ( nMsb == -1 && nLsb == -1 )
+                    {
+                        // get the actual net
+                        pNetActual = Ver_ParseFindNet( pNtk, pWord );
+                        if ( pNetActual == NULL )
+                        {
+                            sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", pWord, Abc_ObjName(pNode) );
+                            Ver_ParsePrintErrorMessage( pMan );
+                            return 0;
+                        }
+                        Vec_PtrPush( pBundle->vNetsActual, pNetActual );
+                        i++;
+                    }
+                    else
+                    {
+                        // go from MSB to LSB
+                        assert( nMsb >= 0 && nLsb >= 0 );
+                        Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1;  
+                        for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--, i++ )
+                        {
+                            // get the actual net
+                            sprintf( Buffer, "%s[%d]", pWord, Bit );
+                            pNetActual = Ver_ParseFindNet( pNtk, Buffer );
+                            if ( pNetActual == NULL )
+                            {
+                                sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", Buffer, Abc_ObjName(pNode) );
+                                Ver_ParsePrintErrorMessage( pMan );
+                                return 0;
+                            }
+                            Vec_PtrPush( pBundle->vNetsActual, pNetActual );
+                        }
+                    }
+                }
+
+                if ( fQuit )
+                    break;
+
+                // skip comma
+                Ver_ParseSkipComments( pMan );
+                Symbol = Ver_StreamPopChar(p);
+                if ( Symbol == '}' )
+                    break;
+                if ( Symbol != ',' )
+                {
+                    sprintf( pMan->sError, "Cannot parse formal parameter %s of gate %s (expected comma).", pWord, Abc_ObjName(pNode) );
+                    Ver_ParsePrintErrorMessage( pMan );
+                    return 0;
+                }
+            }
         }
         else
         {
+            // get the next word
+            pWord = Ver_ParseGetName( pMan );
+            if ( pWord == NULL )
+                return 0;
+            // consider the case of empty name
+            fCompl = 0;
+            if ( pWord[0] == 0 )
+            {
+                pNetActual = Abc_NtkCreateNet( pNtk );
+            }
+            else
+            {
 /*
             // check if the name is complemented
             fCompl = (pWord[0] == '~');
@@ -1307,34 +1729,39 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
                     pNtk->pData = Extra_MmFlexStart();
             }
 */
-            // get the actual net
-            pNetActual = Ver_ParseFindNet( pNtk, pWord );
-            if ( pNetActual == NULL )
-            {
-                sprintf( pMan->sError, "Actual net is missing in gate %s.", Abc_ObjName(pNode) );
-                Ver_ParsePrintErrorMessage( pMan );
-                return 0;
+                // get the actual net
+                pNetActual = Ver_ParseFindNet( pNtk, pWord );
+                if ( pNetActual == NULL )
+                {
+                    sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", pWord, Abc_ObjName(pNode) );
+                    Ver_ParsePrintErrorMessage( pMan );
+                    return 0;
+                }
             }
+            Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
         }
-        Vec_PtrPush( vNetPairs, Abc_ObjNotCond( pNetActual, fCompl ) );
 
-        // close the paranthesis
-        if ( Ver_StreamPopChar(p) != ')' )
+        if ( fFormalIsGiven )
         {
-            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) );
-            Ver_ParsePrintErrorMessage( pMan );
-            return 0;
+            // close the paranthesis
+            Ver_ParseSkipComments( pMan );
+            if ( Ver_StreamPopChar(p) != ')' )
+            {
+                sprintf( pMan->sError, "Cannot parse formal parameter %s of gate %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+            Ver_ParseSkipComments( pMan );
         }
 
         // check if it is the end of gate
-        Ver_ParseSkipComments( pMan );
         Symbol = Ver_StreamPopChar(p);
         if ( Symbol == ')' )
             break;
         // skip comma
         if ( Symbol != ',' )
         {
-            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) );
+            sprintf( pMan->sError, "Cannot parse formal parameter %s of gate %s (expected comma).", pWord, Abc_ObjName(pNode) );
             Ver_ParsePrintErrorMessage( pMan );
             return 0;
         }
@@ -1364,258 +1791,713 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
   SeeAlso     []
 
 ***********************************************************************/
+void Ver_ParseFreeBundle( Ver_Bundle_t * pBundle )
+{
+    FREE( pBundle->pNameFormal );
+    Vec_PtrFree( pBundle->vNetsActual );
+    free( pBundle );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Connects one box to the network]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
 {
-    Vec_Ptr_t * vNetPairs = (Vec_Ptr_t *)pBox->pCopy;
+    Vec_Ptr_t * vBundles = (Vec_Ptr_t *)pBox->pCopy;
     Abc_Ntk_t * pNtk = pBox->pNtk;
     Abc_Ntk_t * pNtkBox = pBox->pData;
-    Abc_Obj_t * pNet, * pTerm, * pTermNew;
-    int i;
+    Abc_Obj_t * pTerm, * pTermNew, * pNetAct;
+    Ver_Bundle_t * pBundle;
+    char * pNameFormal;
+    int i, k, j, iBundle, Length;
 
     assert( !Ver_ObjIsConnected(pBox) );
     assert( Ver_NtkIsDefined(pNtkBox) );
     assert( !Abc_NtkHasBlackbox(pNtkBox) || Abc_NtkBoxNum(pNtkBox) == 1 );
-
+/*
     // clean the PI/PO nets
     Abc_NtkForEachPi( pNtkBox, pTerm, i )
         Abc_ObjFanout0(pTerm)->pCopy = NULL;
     Abc_NtkForEachPo( pNtkBox, pTerm, i )
         Abc_ObjFanin0(pTerm)->pCopy = NULL;
-
-    // map formal nets into actual nets
-    Vec_PtrForEachEntry( vNetPairs, pNet, i )
+*/
+    // check if some of them do not have formal names
+    Vec_PtrForEachEntry( vBundles, pBundle, k )
+        if ( pBundle->pNameFormal == NULL )
+            break;
+    if ( k < Vec_PtrSize(vBundles) )
     {
-        // get the actual net corresponding to this formal net (pNet)
-        pNet->pCopy = Vec_PtrEntry( vNetPairs, ++i );
-        // make sure the actual net is not complemented (otherwise need to use polarity)
-        assert( !Abc_ObjIsComplement(pNet->pCopy) );
+        printf( "Warning: The instance %s of network %s will be connected without using formal names.\n", pNtkBox->pName, Abc_ObjName(pBox) );
+        // add all actual nets in the bundles
+        iBundle = 0;
+        Vec_PtrForEachEntry( vBundles, pBundle, j )
+            iBundle += Vec_PtrSize(pBundle->vNetsActual);
+
+        // check the number of actual nets is the same as the number of formal nets
+        if ( iBundle != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
+        {
+            sprintf( pMan->sError, "The number of actual IOs (%d) is different from the number of formal IOs (%d) when instantiating network %s in box %s.", 
+                Vec_PtrSize(vBundles), Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox), pNtkBox->pName, Abc_ObjName(pBox) );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // connect bundles in the natural order
+        iBundle = 0;
+        Abc_NtkForEachPi( pNtkBox, pTerm, i )
+        {
+            pBundle = Vec_PtrEntry( vBundles, iBundle++ );
+            // the bundle is found - add the connections - using order LSB to MSB
+            Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k )
+            {
+                pTermNew = Abc_NtkCreateBi( pNtk );
+                Abc_ObjAddFanin( pBox, pTermNew );
+                Abc_ObjAddFanin( pTermNew, pNetAct );
+                i++;
+            }
+            i--;
+        }
+        // create fanins of the box
+        Abc_NtkForEachPo( pNtkBox, pTerm, i )
+        {
+            pBundle = Vec_PtrEntry( vBundles, iBundle++ );
+            // the bundle is found - add the connections - using order LSB to MSB
+            Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k )
+            {
+                pTermNew = Abc_NtkCreateBo( pNtk );
+                Abc_ObjAddFanin( pTermNew, pBox );
+                Abc_ObjAddFanin( pNetAct, pTermNew );
+                i++;
+            }
+            i--;
+        }
+
+        // free the bundling
+        Vec_PtrForEachEntry( vBundles, pBundle, k )
+            Ver_ParseFreeBundle( pBundle );
+        Vec_PtrFree( vBundles );
+        pBox->pCopy = NULL;
+        return 1;
     }
 
-    // make sure all PI nets are assigned
+    // bundles arrive in any order - but inside each bundle the order is MSB to LSB
+    // make sure every formal PI has a corresponding net
     Abc_NtkForEachPi( pNtkBox, pTerm, i )
     {
-        if ( Abc_ObjFanout0(pTerm)->pCopy == NULL )
+        // get the name of this formal net
+        pNameFormal = Abc_ObjName( Abc_ObjFanout0(pTerm) );
+        // try to find the bundle with this formal net
+        pBundle = NULL;
+        Vec_PtrForEachEntry( vBundles, pBundle, k )
+            if ( !strcmp(pBundle->pNameFormal, pNameFormal) )
+                break;
+        assert( pBundle != NULL );
+        // if the bundle is not found, try without parantheses
+        if ( k == Vec_PtrSize(vBundles) )
         {
-            sprintf( pMan->sError, "Input formal net %s of network %s is not driven in box %s.", 
-                Abc_ObjName(Abc_ObjFanout0(pTerm)), pNtkBox->pName, Abc_ObjName(pBox) );
-            Ver_ParsePrintErrorMessage( pMan );
-            return 0;
+            pBundle = NULL;
+            Length = strlen(pNameFormal);
+            if ( pNameFormal[Length-1] == ']' )
+            {
+                // find the opening brace
+                for ( Length--; Length >= 0; Length-- )
+                    if ( pNameFormal[Length] == '[' )
+                        break;
+                // compare names before brace
+                if ( Length > 0 )
+                {
+                    Vec_PtrForEachEntry( vBundles, pBundle, j )
+                        if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) )
+                            break;
+                    if ( j == Vec_PtrSize(vBundles) )
+                        pBundle = NULL;
+                }
+            }
+            if ( pBundle == NULL )
+            {
+                sprintf( pMan->sError, "Cannot find an actual net for the formal net %s when instantiating network %s in box %s.", 
+                    pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+        }
+        // the bundle is found - add the connections - using order LSB to MSB
+        Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k )
+        {
+            pTermNew = Abc_NtkCreateBi( pNtk );
+            Abc_ObjAddFanin( pBox, pTermNew );
+            Abc_ObjAddFanin( pTermNew, pNetAct );
+            i++;
         }
-        pTermNew = Abc_NtkCreateBi( pNtk );
-        Abc_ObjAddFanin( pBox, pTermNew );
-        Abc_ObjAddFanin( pTermNew, Abc_ObjFanout0(pTerm)->pCopy );
+        i--;
     }
 
-    // create fanins of the box
+    // connect those formal POs that do have nets
     Abc_NtkForEachPo( pNtkBox, pTerm, i )
     {
-        if ( Abc_ObjFanin0(pTerm)->pCopy == NULL )
-            Abc_ObjFanin0(pTerm)->pCopy = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET );
-        pTermNew = Abc_NtkCreateBo( pNtk );
-        Abc_ObjAddFanin( Abc_ObjFanin0(pTerm)->pCopy, pTermNew );
-        Abc_ObjAddFanin( pTermNew, pBox );
+        // get the name of this PI
+        pNameFormal = Abc_ObjName( Abc_ObjFanin0(pTerm) );
+        // try to find this formal net in the bundle
+        pBundle = NULL;
+        Vec_PtrForEachEntry( vBundles, pBundle, k )
+            if ( !strcmp(pBundle->pNameFormal, pNameFormal) )
+                break;
+        assert( pBundle != NULL );
+        // if the name is not found, try without parantheses
+        if ( k == Vec_PtrSize(vBundles) )
+        {
+            pBundle = NULL;
+            Length = strlen(pNameFormal);
+            if ( pNameFormal[Length-1] == ']' )
+            {
+                // find the opening brace
+                for ( Length--; Length >= 0; Length-- )
+                    if ( pNameFormal[Length] == '[' )
+                        break;
+                // compare names before brace
+                if ( Length > 0 )
+                {
+                    Vec_PtrForEachEntry( vBundles, pBundle, j )
+                        if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) )
+                            break;
+                    if ( j == Vec_PtrSize(vBundles) )
+                        pBundle = NULL;
+                }
+            }
+            if ( pBundle == NULL )
+            {
+                printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.", 
+                    pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
+                continue;
+            }
+        }
+        // the bundle is found - add the connections
+        Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k )
+        {
+            if ( !strcmp(Abc_ObjName(pNetAct), "1\'b0") || !strcmp(Abc_ObjName(pNetAct), "1\'b1") )
+            {
+                sprintf( pMan->sError, "It looks like formal output %s is driving a constant net (%s) when instantiating network %s in box %s.", 
+                    pBundle->pNameFormal, Abc_ObjName(pNetAct), pNtkBox->pName, Abc_ObjName(pBox) );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+            pTermNew = Abc_NtkCreateBo( pNtk );
+            Abc_ObjAddFanin( pTermNew, pBox );
+            Abc_ObjAddFanin( pNetAct, pTermNew );
+            i++;
+        }
+        i--;
     }
 
-    // free the mapping
-    Vec_PtrFree( vNetPairs );
+    // free the bundling
+    Vec_PtrForEachEntry( vBundles, pBundle, k )
+        Ver_ParseFreeBundle( pBundle );
+    Vec_PtrFree( vBundles );
     pBox->pCopy = NULL;
     return 1;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Attaches the boxes to the network.]
+  Synopsis    [Connects the defined boxes.]
 
-  Description [Makes sure that the undefined boxes are connected correctly.]
+  Description [Returns 2 if there are any undef boxes.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Vec_ParseAttachBoxes( Ver_Man_t * pMan )
+int Ver_ParseConnectDefBoxes( Ver_Man_t * pMan )
 {
-    Abc_Ntk_t * pNtk, * pNtkBox;
-    Vec_Ptr_t * vEnvoys, * vNetPairs, * vPivots;
-    Abc_Obj_t * pBox, * pTerm, * pNet, * pNetDr, * pNetAct;
-    int i, k, m, nBoxes;
-
-    // connect defined boxes
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pBox;
+    int i, k, RetValue = 1;
+    // go through all the modules
     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
     {
-        Abc_NtkForEachBlackbox( pNtk, pBox, k )
+        // go through all the boxes of this module
+        Abc_NtkForEachBox( pNtk, pBox, k )
         {
-            if ( pBox->pData && Ver_NtkIsDefined(pBox->pData) )
-                if ( !Ver_ParseConnectBox( pMan, pBox ) )
-                    return 0;
+            if ( Abc_ObjIsLatch(pBox) )
+                continue;
+            // skip internal boxes of the blackboxes
+            if ( pBox->pData == NULL )
+                continue;
+            // if the network is undefined, it will be connected later
+            if ( !Ver_NtkIsDefined(pBox->pData) )
+            {
+                RetValue = 2;
+                continue;
+            }
+            // connect the box
+            if ( !Ver_ParseConnectBox( pMan, pBox ) )
+                return 0;
+            // if the network is a true blackbox, skip
+            if ( Abc_NtkHasBlackbox(pBox->pData) )
+                continue;
+            // convert the box to the whitebox
+            Abc_ObjBlackboxToWhitebox( pBox );
         }
     }
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the undef boxes and maps them into their instances.]
 
-    // convert blackboxes to whiteboxes
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ver_ParseCollectUndefBoxes( Ver_Man_t * pMan )
+{
+    Vec_Ptr_t * vUndefs;
+    Abc_Ntk_t * pNtk, * pNtkBox;
+    Abc_Obj_t * pBox;
+    int i, k;
+    // clear the module structures
     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+        pNtk->pData = NULL;
+    // go through all the blackboxes
+    vUndefs = Vec_PtrAlloc( 16 );
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+    {
         Abc_NtkForEachBlackbox( pNtk, pBox, k )
         {
             pNtkBox = pBox->pData;
             if ( pNtkBox == NULL )
                 continue;
-
-            if ( !strcmp( pNtkBox->pName, "ADDHX1" ) )
+            if ( Ver_NtkIsDefined(pNtkBox) )
+                continue;
+            if ( pNtkBox->pData == NULL )
             {
-                int x = 0;
+                // save the box
+                Vec_PtrPush( vUndefs, pNtkBox );
+                pNtkBox->pData = Vec_PtrAlloc( 16 );
             }
+            // save the instance
+            Vec_PtrPush( pNtkBox->pData, pBox );
+        }
+    }
+    return vUndefs;
+}
 
-            if ( pBox->pData && !Abc_NtkHasBlackbox(pBox->pData) )
-                Abc_ObjBlackboxToWhitebox( pBox );
-        }   
+/**Function*************************************************************
 
+  Synopsis    [Reports how many times each type of undefined box occurs.]
 
-    // search for undefined boxes
-    nBoxes = 0;
-    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
-        nBoxes += !Ver_NtkIsDefined(pNtk);
-    // quit if no undefined boxes are found
-    if ( nBoxes == 0 )
-        return 1;
+  Description []
+               
+  SideEffects []
 
-    // count how many times each box occurs
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_ParseReportUndefBoxes( Ver_Man_t * pMan )
+{
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pBox;
+    int i, k, nBoxes;
+    // clean 
+    nBoxes = 0;
     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
     {
-        assert( pNtk->pData == NULL );
-        pNtk->pData = NULL;
+        pNtk->fHiePath = 0;
+        if ( !Ver_NtkIsDefined(pNtk) )
+            nBoxes++;
     }
+    // count
     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
         Abc_NtkForEachBlackbox( pNtk, pBox, k )
-        {
-            if ( pBox->pData == NULL )
-                continue;
-            pNtkBox = pBox->pData;
-            pNtkBox->pData = (void *)((int)pNtkBox->pData + 1);
-        }
-
-    // print the boxes
+            if ( pBox->pData && !Ver_NtkIsDefined(pBox->pData) )
+                ((Abc_Ntk_t *)pBox->pData)->fHiePath++;
+    // print the stats
     printf( "Warning: The design contains %d undefined objects interpreted as blackboxes:\n", nBoxes );
     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
         if ( !Ver_NtkIsDefined(pNtk) )
-            printf( "%s (%d)  ", Abc_NtkName(pNtk), (int)pNtk->pData );
+            printf( "%s (%d)  ", Abc_NtkName(pNtk), pNtk->fHiePath );
     printf( "\n" );
-
-    // clean the boxes
+    // clean 
     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
-        pNtk->pData = NULL;
+        pNtk->fHiePath = 0;
+}
 
+/**Function*************************************************************
 
-    // map actual nets into formal nets belonging to the undef boxes
-    vPivots = Vec_PtrAlloc( 100 );
-    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
-    {
-        Abc_NtkForEachBlackbox( pNtk, pBox, k )
-        {
-            if ( pBox->pData == NULL || Ver_NtkIsDefined(pBox->pData) )
-                continue;
-            vNetPairs = (Vec_Ptr_t *)pBox->pCopy;
-            Vec_PtrForEachEntry( vNetPairs, pNet, m )
-            {
-                pNetAct = Vec_PtrEntry( vNetPairs, ++m );
-                // skip already driven nets and constants
-                if ( Abc_ObjFaninNum(pNetAct) == 1 )
-                    continue;
-                if ( !(strcmp(Abc_ObjName(pNetAct), "1\'b0") && strcmp(Abc_ObjName(pNetAct), "1\'b1")) ) // constant
-                    continue;
-                // add this net
-                if ( pNetAct->pData == NULL )
+  Synopsis    [Returns 1 if there are non-driven nets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseCheckNondrivenNets( Vec_Ptr_t * vUndefs )
+{
+    Abc_Ntk_t * pNtk;
+    Ver_Bundle_t * pBundle;
+    Abc_Obj_t * pBox, * pNet;
+    int i, k, j, m;
+    // go through undef box types
+    Vec_PtrForEachEntry( vUndefs, pNtk, i )
+        // go through instances of this type
+        Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+            // go through the bundles of this instance
+            Vec_PtrForEachEntryReverse( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
+                // go through the actual nets of this bundle
+                if ( pBundle )
+                Vec_PtrForEachEntry( pBundle->vNetsActual, pNet, m )
                 {
-                    pNetAct->pData = Vec_PtrAlloc( 16 );
-                    Vec_PtrPush( vPivots, pNetAct );
+                    char * pName = Abc_ObjName(pNet);
+                    if ( Abc_ObjFaninNum(pNet) == 0 ) // non-driven
+                        if ( strcmp(Abc_ObjName(pNet), "1\'b0") && strcmp(Abc_ObjName(pNet), "1\'b1") ) // diff from a const
+                            return 1;
                 }
-                vEnvoys = pNetAct->pData;
-                Vec_PtrPush( vEnvoys, pNet );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if formal nets with the given name are driven in any of the instances of undef boxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseFormalNetsAreDriven( Abc_Ntk_t * pNtk, char * pNameFormal )
+{
+    Ver_Bundle_t * pBundle;
+    Abc_Obj_t * pBox, * pNet;
+    int k, j, m;
+    // go through instances of this type
+    Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+    {
+        // find a bundle with the given name in this instance
+        Vec_PtrForEachEntryReverse( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
+            if ( pBundle && !strcmp( pBundle->pNameFormal, pNameFormal ) )
+                break;
+        // skip non-driven bundles
+        if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
+            continue;
+        // check if all nets are driven in this bundle
+        Vec_PtrForEachEntry( pBundle->vNetsActual, pNet, m )
+            if ( Abc_ObjFaninNum(pNet) > 0 )
+                return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the non-driven bundle that is given distance from the end.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ver_Bundle_t * Ver_ParseGetNondrivenBundle( Abc_Ntk_t * pNtk, int Counter )
+{
+    Ver_Bundle_t * pBundle;
+    Abc_Obj_t * pBox, * pNet;
+    int k, m;
+    // go through instances of this type
+    Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+    {
+        if ( Counter >= Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
+            continue;
+        // get the bundle given distance away
+        pBundle = Vec_PtrEntry( (Vec_Ptr_t *)pBox->pCopy, Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) - 1 - Counter );
+        if ( pBundle == NULL )
+            continue;
+        // go through the actual nets of this bundle
+        Vec_PtrForEachEntry( pBundle->vNetsActual, pNet, m )
+            if ( !Abc_ObjFaninNum(pNet) && !Ver_ParseFormalNetsAreDriven(pNtk, pBundle->pNameFormal) ) // non-driven
+                return pBundle;
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Drives the bundle in the given undef box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseDriveFormal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_Bundle_t * pBundle0 )
+{
+    char Buffer[200];
+    char * pName;
+    Ver_Bundle_t * pBundle;
+    Abc_Obj_t * pBox, * pTerm, * pTermNew, * pNetAct, * pNetFormal;
+    int k, j, m;
+
+    // drive this net in the undef box
+    Vec_PtrForEachEntry( pBundle0->vNetsActual, pNetAct, m )
+    {
+        // create the formal net
+        if ( Vec_PtrSize(pBundle0->vNetsActual) == 1 )
+            sprintf( Buffer, "%s", pBundle0->pNameFormal );
+        else
+            sprintf( Buffer, "%s[%d]", pBundle0->pNameFormal, m );
+        assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL );
+        pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer );
+        // connect it to the box
+        pTerm = Abc_NtkCreateBo( pNtk );
+        assert( Abc_NtkBoxNum(pNtk) <= 1 );
+        pBox = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk);
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtk), pNetFormal );
+        Abc_ObjAddFanin( pNetFormal, pTerm );
+        Abc_ObjAddFanin( pTerm, pBox );
+    }
+
+    // go through instances of this type
+    pName = Extra_UtilStrsav(pBundle0->pNameFormal);
+    Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+    {
+        // find a bundle with the given name in this instance
+        Vec_PtrForEachEntryReverse( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
+            if ( pBundle && !strcmp( pBundle->pNameFormal, pName ) )
+                break;
+        // skip non-driven bundles
+        if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
+            continue;
+        // check if any nets are driven in this bundle
+        Vec_PtrForEachEntry( pBundle->vNetsActual, pNetAct, m )
+            if ( Abc_ObjFaninNum(pNetAct) > 0 )
+            {
+                sprintf( pMan->sError, "Internal error while trying to connect undefined boxes. It is likely that the algorithm currently used has its limitations." );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
             }
+        // drive the nets by the undef box
+        Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, m )
+        {
+            pTermNew = Abc_NtkCreateBo( pNetAct->pNtk );
+            Abc_ObjAddFanin( pTermNew, pBox );
+            Abc_ObjAddFanin( pNetAct, pTermNew );
         }
+        // remove the bundle
+        Ver_ParseFreeBundle( pBundle );
+        Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
     }
+    free( pName );
+    return 1;
+}
+
 
-    // for each pivot net, find the driver
-    Vec_PtrForEachEntry( vPivots, pNetAct, i )
+/**Function*************************************************************
+
+  Synopsis    [Drives the bundle in the given undef box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseDriveInputs( Ver_Man_t * pMan, Vec_Ptr_t * vUndefs )
+{
+    char Buffer[200];
+    Ver_Bundle_t * pBundle;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pBox, * pBox2, * pTerm, * pTermNew, * pNetFormal, * pNetAct;
+    int i, k, j, m, CountCur, CountTotal = -1;
+    // iterate through the undef boxes
+    Vec_PtrForEachEntry( vUndefs, pNtk, i )
     {
-        char * pName = Abc_ObjName(pNetAct);
-/*
-        if ( !strcmp( Abc_ObjName(pNetAct), "dma_fifo_ff_cnt[2]" ) )
+        // count the number of unconnected bundles for instances of this type of box
+        CountTotal = -1;
+        Vec_PtrForEachEntry( pNtk->pData, pBox, k )
         {
-            int x = 0;
+            CountCur = 0;
+            Vec_PtrForEachEntry( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
+                CountCur += (pBundle != NULL);
+            if ( CountTotal == -1 )
+                CountTotal = CountCur;
+            else if ( CountTotal != CountCur )
+            {
+                sprintf( pMan->sError, "The number of formal inputs (%d) is different from the expected one (%d) when instantiating network %s in box %s.", 
+                    CountCur, CountTotal, pNtk->pName, Abc_ObjName(pBox) );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
         }
-*/
-        assert( Abc_ObjFaninNum(pNetAct) == 0 );
-        assert( strcmp(Abc_ObjName(pNetAct), "1\'b0") && strcmp(Abc_ObjName(pNetAct), "1\'b1") );
-        vEnvoys = pNetAct->pData; pNetAct->pData = NULL;
-        // find the driver starting from the last nets
-        pNetDr = NULL;
-        for ( m = 0; m < 64; m++ )
+
+        // create formals
+        pBox = Vec_PtrEntry( pNtk->pData, 0 );
+        Vec_PtrForEachEntry( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
         {
-            Vec_PtrForEachEntry( vEnvoys, pNet, k )
+            if ( pBundle == NULL )
+                continue;
+            Vec_PtrForEachEntry( pBundle->vNetsActual, pNetAct, m )
+            {
+                // find create the formal net
+                if ( Vec_PtrSize(pBundle->vNetsActual) == 1 )
+                    sprintf( Buffer, "%s", pBundle->pNameFormal );
+                else
+                    sprintf( Buffer, "%s[%d]", pBundle->pNameFormal, m );
+                assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL );
+                pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer );
+                // connect
+                pTerm = Abc_NtkCreateBi( pNtk );
+                assert( Abc_NtkBoxNum(pNtk) <= 1 );
+                pBox2 = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk);
+                Abc_ObjAddFanin( pNetFormal, Abc_NtkCreatePi(pNtk) );
+                Abc_ObjAddFanin( pTerm, pNetFormal );
+                Abc_ObjAddFanin( pBox2, pTerm );
+            }
+        }
+
+        // go through all the boxes
+        Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+        {
+            // go through all the bundles
+            Vec_PtrForEachEntry( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
             {
-                if ( Abc_ObjId(pNet) == 0 )
+                if ( pBundle == NULL )
                     continue;
-                if ( (int)Abc_ObjId(pNet) == Abc_NtkObjNumMax(pNet->pNtk) - 1 - m )
+                // drive the nets by the undef box
+                Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, m )
                 {
-                    pNetDr = pNet;
-                    break;
+                    pTermNew = Abc_NtkCreateBi( pNetAct->pNtk );
+                    Abc_ObjAddFanin( pBox, pTermNew );
+                    Abc_ObjAddFanin( pTermNew, pNetAct );
                 }
+                // remove the bundle
+                Ver_ParseFreeBundle( pBundle );
+                Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
             }
-            if ( pNetDr )
-                break;
+
+            // free the bundles
+            Vec_PtrFree( (Vec_Ptr_t *)pBox->pCopy );
+            pBox->pCopy = NULL;
         }
-        assert( pNetDr != NULL );
-        Vec_PtrWriteEntry( vPivots, i, pNetDr );
-        Vec_PtrFree( vEnvoys );
     }
+    return 1;
+}
 
-    // for each pivot net, create driver
-    Vec_PtrForEachEntry( vPivots, pNetDr, i )
-    {
-        if ( pNetDr == NULL )
-            continue;
-        assert( Abc_ObjFaninNum(pNetDr) <= 1 );
-        if ( Abc_ObjFaninNum(pNetDr) == 1 )
-            continue;
-        // drive this net with the box
-        pTerm = Abc_NtkCreateBo( pNetDr->pNtk );
-        assert( Abc_NtkBoxNum(pNetDr->pNtk) <= 1 );
-        pBox = Abc_NtkBoxNum(pNetDr->pNtk)? Abc_NtkBox(pNetDr->pNtk,0) : Abc_NtkCreateBlackbox(pNetDr->pNtk);
-        Abc_ObjAddFanin( Abc_NtkCreatePo(pNetDr->pNtk), pNetDr );
-        Abc_ObjAddFanin( pNetDr, pTerm );
-        Abc_ObjAddFanin( pTerm, pBox );
-    }
-    Vec_PtrFree( vPivots );
 
-    // connect the remaining boxes
-    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+/**Function*************************************************************
+
+  Synopsis    [Returns the max size of any undef box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseMaxBoxSize( Vec_Ptr_t * vUndefs )
+{
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pBox;
+    int i, k, nMaxSize = 0;
+    // go through undef box types
+    Vec_PtrForEachEntry( vUndefs, pNtk, i )
+        // go through instances of this type
+        Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+            // check the number of bundles of this instance
+            if ( nMaxSize < Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
+                nMaxSize = Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy);
+    return nMaxSize;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Attaches the boxes to the network.]
+
+  Description [This procedure is called after the design is parsed. 
+  At that point, all the defined models have their PIs present. 
+  They are connected first. Next undef boxes are processed (if present).
+  Iteratively, one bundle is selected to be driven by the undef boxes in such 
+  a way that there is no conflict (if it is driven by an instance of the box,
+  no other net will be driven twice by the same formal net of some other instance 
+  of the same box). In the end, all the remaining nets that cannot be driven 
+  by the undef boxes are connected to the undef boxes as inputs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseAttachBoxes( Ver_Man_t * pMan )
+{
+    Abc_Ntk_t * pNtk;
+    Ver_Bundle_t * pBundle;
+    Vec_Ptr_t * vUndefs;
+    int i, RetValue, Counter, nMaxBoxSize;
+
+    // connect defined boxes
+    RetValue = Ver_ParseConnectDefBoxes( pMan );
+    if ( RetValue < 2 )
+        return RetValue;
+
+    // report the boxes
+    Ver_ParseReportUndefBoxes( pMan );
+
+    // collect undef box types and their actual instances
+    vUndefs = Ver_ParseCollectUndefBoxes( pMan );
+    assert( Vec_PtrSize( vUndefs ) > 0 );
+
+    // go through all undef box types
+    Counter = 0;
+    nMaxBoxSize = Ver_ParseMaxBoxSize( vUndefs );
+    while ( Ver_ParseCheckNondrivenNets(vUndefs) && Counter < nMaxBoxSize )
     {
-        if ( Abc_NtkPiNum(pNtk) )
-            continue;
-        Abc_NtkForEachNet( pNtk, pNet, k )
+        // go through undef box types
+        pBundle = NULL;
+        Vec_PtrForEachEntry( vUndefs, pNtk, i )
+            if ( pBundle = Ver_ParseGetNondrivenBundle( pNtk, Counter ) )
+                break;
+        if ( pBundle == NULL )
         {
-            if ( Abc_ObjFaninNum(pNet) )
-                continue;
-            // drive this net
-            pTerm = Abc_NtkCreateBi( pNet->pNtk );
-            assert( Abc_NtkBoxNum(pNet->pNtk) <= 1 );
-            pBox = Abc_NtkBoxNum(pNet->pNtk)? Abc_NtkBox(pNet->pNtk,0) : Abc_NtkCreateBlackbox(pNet->pNtk);
-            Abc_ObjAddFanin( pBox, pTerm );
-            Abc_ObjAddFanin( pTerm, pNet );
-            Abc_ObjAddFanin( pNet, Abc_NtkCreatePi(pNet->pNtk) );
+            Counter++;
+            continue;
         }
+        // drive this bundle by this box
+        if ( !Ver_ParseDriveFormal( pMan, pNtk, pBundle ) )
+            return 0;
     }
 
-    // connect the remaining boxes
-    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+    // make all the remaining bundles the drivers of undefs
+    if ( !Ver_ParseDriveInputs( pMan, vUndefs ) )
+        return 0;
+
+    // cleanup
+    Vec_PtrForEachEntry( vUndefs, pNtk, i )
     {
-        Abc_NtkForEachBlackbox( pNtk, pBox, k )
-        {
-            char * pName = Abc_ObjName(pBox);
-            if ( !Ver_ObjIsConnected(pBox) )
-                if ( !Ver_ParseConnectBox( pMan, pBox ) )
-                    return 0;
-        }
+        Vec_PtrFree( pNtk->pData );
+        pNtk->pData = NULL;
     }
+    Vec_PtrFree( vUndefs ); 
     return 1;
 }
 
@@ -1716,55 +2598,12 @@ Abc_Obj_t * Ver_ParseCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet )
 {
     Abc_Obj_t * pObj;
     pObj = Abc_NtkCreateNodeInv( pNtk, pNet );
-    pNet = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET );
+    pNet = Abc_NtkCreateNet( pNtk );
     Abc_ObjAddFanin( pNet, pObj );
     return pNet;
 }
 
 
-
-/*
-    // allocate memory to remember the phase
-    pPolarity = NULL;
-    if ( fComplUsed )
-    {
-        int nBytes = 4 * Abc_BitWordNum( Abc_NtkPiNum(pNtkBox) );
-        pPolarity = (unsigned *)Extra_MmFlexEntryFetch( pNtk->pData, nBytes );
-        memset( pPolarity, 0, nBytes );
-    }
-    // create box to represent this gate
-    if ( Abc_NtkHasBlackbox(pNtkBox) )
-        pNode = Abc_NtkCreateBlackbox( pNtk );
-    else
-        pNode = Abc_NtkCreateWhitebox( pNtk );
-    pNode->pNext = (Abc_Obj_t *)pPolarity;
-    pNode->pData = pNtkBox;
-    // connect to fanin nets
-    Abc_NtkForEachPi( pNtkBox, pObj, i )
-    {
-        if ( pPolarity && Abc_ObjIsComplement(pObj->pCopy) )
-        {
-            Abc_InfoSetBit( pPolarity, i );
-            pObj->pCopy = Abc_ObjRegular( pObj->pCopy );
-        }
-        assert( !Abc_ObjIsComplement(pObj->pCopy) );
-//        Abc_ObjAddFanin( pNode, pObj->pCopy );
-        pTerm = Abc_NtkCreateBi( pNtk );
-        Abc_ObjAddFanin( pTerm, pObj->pCopy );
-        Abc_ObjAddFanin( pNode, pTerm );
-    }
-    // connect to fanout nets
-    Abc_NtkForEachPo( pNtkBox, pObj, i )
-    {
-        if ( pObj->pCopy == NULL )
-            pObj->pCopy = Abc_NtkFindOrCreateNet(pNtk, NULL);
-//        Abc_ObjAddFanin( pObj->pCopy, pNode );
-        pTerm = Abc_NtkCreateBo( pNtk );
-        Abc_ObjAddFanin( pTerm, pNode );
-        Abc_ObjAddFanin( pObj->pCopy, pTerm );
-    }
-*/
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/ver/verCore.zip b/src/base/ver/verCore.zip
new file mode 100644
index 00000000..481f7e6a
--- /dev/null
+++ b/src/base/ver/verCore.zip
diff --git a/src/base/ver/verFormula.c b/src/base/ver/verFormula.c
index 253754ae..19a2c523 100644
--- a/src/base/ver/verFormula.c
+++ b/src/base/ver/verFormula.c
@@ -120,7 +120,7 @@ void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_
         case '\r':
         case '\n':
             continue;
-
+/*
         // treat Constant 0 as a variable
         case VER_PARSE_SYM_CONST0:
             Vec_PtrPush( vStackFn, Hop_ManConst0(pMan) );  // Cudd_Ref( Hop_ManConst0(pMan) );
@@ -144,7 +144,7 @@ void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_
             }
             Flag = VER_PARSE_FLAG_VAR; 
             break;
-
+*/
         case VER_PARSE_SYM_NEGBEF1:
         case VER_PARSE_SYM_NEGBEF2:
             if ( Flag == VER_PARSE_FLAG_VAR )