Version abc70225

13 files changed, 1370 insertions, 355 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 \