Version abc70225

Makefile

@@ -23,7 +23,7 @@ OPTFLAGS  := -g -O
 CFLAGS   += -Wall -Wno-unused-function $(OPTFLAGS) $(patsubst %, -I%, $(MODULES)) 
 CXXFLAGS += $(CFLAGS) 
 
-LIBS := -ldl -rdynamic -lreadline -ltermcap libhmetis.a
+LIBS := -ldl -rdynamic -lreadline -ltermcap
 SRC  := 
 GARBAGE := core core.* *.stackdump ./tags $(PROG)
 

abc.dsp

@@ -50,7 +50,7 @@ BSC32=bscmake.exe
 # ADD BSC32 /nologo
 LINK32=link.exe
 # ADD BASE LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /machine:I386
-# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib lib/libhmetis.lib /nologo /subsystem:console /profile /machine:I386 /out:"_TEST/abc.exe"
+# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /profile /machine:I386 /out:"_TEST/abc.exe"
 
 !ELSEIF  "$(CFG)" == "abc - Win32 Debug"
 
@@ -75,7 +75,7 @@ BSC32=bscmake.exe
 # ADD BSC32 /nologo
 LINK32=link.exe
 # ADD BASE LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /debug /machine:I386 /pdbtype:sept
-# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib lib/libhmetis.lib /nologo /subsystem:console /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept
+# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept
 
 !ENDIF 
 
@@ -102,6 +102,10 @@ SOURCE=.\src\base\abc\abcAig.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abc\abcBlifMv.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abc\abcCheck.c
 # End Source File
 # Begin Source File
@@ -1990,10 +1994,6 @@ SOURCE=.\src\map\if\ifMap.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\map\if\ifPrepro.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\map\if\ifReduce.c
 # End Source File
 # Begin Source File

src/aig/mem/mem.c

@@ -278,6 +278,22 @@ int Mem_FixedReadMemUsage( Mem_Fixed_t * p )
     return p->nMemoryAlloc;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mem_FixedReadMaxEntriesUsed( Mem_Fixed_t * p )
+{
+    return p->nEntriesMax;
+}
+
 
 
 /**Function*************************************************************

src/aig/mem/mem.h

@@ -45,6 +45,7 @@ extern char *        Mem_FixedEntryFetch( Mem_Fixed_t * p );
 extern void          Mem_FixedEntryRecycle( Mem_Fixed_t * p, char * pEntry );
 extern void          Mem_FixedRestart( Mem_Fixed_t * p );
 extern int           Mem_FixedReadMemUsage( Mem_Fixed_t * p );
+extern int           Mem_FixedReadMaxEntriesUsed( Mem_Fixed_t * p );
 // flexible-size-block memory manager
 extern Mem_Flex_t *  Mem_FlexStart();
 extern void          Mem_FlexStop( Mem_Flex_t * p, int fVerbose );

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 );

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                                ///
+////////////////////////////////////////////////////////////////////////
+
+

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                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abc/abcDfs.c

@@ -884,6 +884,7 @@ int Abc_NtkLevelReverse_rec( Abc_Obj_t * pNode )
         if ( pNode->Level < (unsigned)Level )
             pNode->Level = 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, "Node \"%s\" is encountered twice on the following path:\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
-        fprintf( stdout, " %s", Abc_ObjIsNode(pNode)? Abc_ObjName(pNode) : Abc_NtkName(pNode->pData) );
+        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;

src/base/abc/abcFunc.c

@@ -878,6 +878,22 @@ int Abc_NtkMapToSop( Abc_Ntk_t * pNtk )
     return 1;
 }
 
+/**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.]

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
+    if ( pNtk->pDesign )
-    assert( Vec_PtrEntry(pNtk->pDesign->vModules, 0) == pNtk );
+    {
+        // 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                                ///
 ////////////////////////////////////////////////////////////////////////

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*************************************************************

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;

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" );
+    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" );
+    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,13 +914,6 @@ 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 );
         // add the fanout net
         Abc_ObjAddFanin( pNet, pNode );
@@ -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) );

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 );

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                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abc/abcUtil.c

@@ -53,43 +53,6 @@ void * Abc_NtkAttrFree( Abc_Ntk_t * pNtk, int Attr, int fFreeMan )
     return pUserMan;
 }
 
-/**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.]
@@ -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) )

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 \

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 );
@@ -1394,6 +1396,64 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  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    []
@@ -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 );  

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 )
+    if ( 1.0 * Abc_NtkObjNum(pNtk) * pIfMan->nObjBytes / (1<<30) > 1.0 )
-        printf( "Warning: The mapper is about to allocate %.1f Gb for to represent %d cuts per node.\n", 
+        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->nEntrySize / (1<<30), pPars->nCutsMax );
+            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;

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 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;
 
@@ -109,6 +114,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
     {
         assert( s_vMemory == NULL );
         s_vMemory  = Vec_IntAlloc( 1 << 16 );
+        s_vMemory2 = Vec_IntAlloc( 1 << 16 );
     }
 
     // perform mapping/renoding
@@ -125,12 +131,43 @@ 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;
 }
 
+/**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.]
@@ -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 )
 {
+    int i, RetValue;
+    // set internal mapper parameters
     for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
-            pCut->pPerm[i] = 100;
+        pCut->pPerm[i] = 1;
-        return ABC_INFINITY;
+    // compute ISOP for the positive phase
-    }
+    RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 );
-    nNodes = Kit_GraphNodeNum( pGraph );
+    if ( RetValue == -1 )
-    for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
+        return IF_COST_MAX;
-        pCut->pPerm[i] = Kit_GraphLeafDepth_rec( pGraph, Kit_GraphNodeLast(pGraph), Kit_GraphNode(pGraph, i) );
+    assert( RetValue == 0 || RetValue == 1 );
-    Kit_GraphFree( pGraph );
+    // compute ISOP for the negative phase
-    return nNodes;
+    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;
 }
 
 ////////////////////////////////////////////////////////////////////////

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" );

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_WriteBlifMv( Abc_Ntk_t * pNtk, char * FileName );
-extern void               Io_WriteBlifMvNetlist( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteBench.c =========================================================*/
 extern int                Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteCnf.c ===========================================================*/

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" );
+//Io_WriteBlifMv( pNtk, "_temp_.mv" );
-//Abc_LibPrint( pDesign );
-//Abc_LibFree( pDesign );
-//return NULL;
     return pNtk;
 }
 
@@ -691,6 +704,7 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
                 return NULL;
             }
             // create binary latch with 1-data and 0-init
+            if ( p->fUseReset ) 
                 pMod->pResetLatch = Io_ReadCreateResetLatch( pMod->pNtk, p->fBlifMv );
         }
         // parse the latches
@@ -698,6 +712,7 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
             if ( !Io_MvParseLineLatch( pMod, pLine ) )
                 return NULL;
         // parse the reset lines
+        if ( p->fUseReset )
             Vec_PtrForEachEntry( pMod->vResets, pLine, k )
                 if ( !Io_MvParseLineNamesMv( pMod, pLine, 1 ) )
                     return NULL;
@@ -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,6 +856,10 @@ 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 ( p->pMan->fBlifMv )
+            Abc_LatchSetInit0( pObj );
+        else
+        {
             if ( Vec_PtrSize(vTokens) > 3 )
                 Init = atoi( Vec_PtrEntry(vTokens,3) );
             else
@@ -854,17 +876,15 @@ static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine )
             else // if ( Init == 2 )
                 Abc_LatchSetInitDc( pObj );
         }
+    }
     else
     {
-        // get the net corresponding to output of reset latch
+        // get the net corresponding to the output of the latch
-        pNet = Abc_ObjFanout0(Abc_ObjFanout0(p->pResetLatch));
+        pNet = Abc_NtkFindOrCreateNet( p->pNtk, Vec_PtrEntry(vTokens,2) );
-        assert( Abc_ObjIsNet(pNet) );
+        // get the net corresponding to the latch output (feeding into reset MUX)
-        // create mux
+        pNet = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pNet, "_out") );
-        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);
         // 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] == '.' )
@@ -1215,6 +1235,60 @@ static char * Io_MvParseTableMv( Io_MvMod_t * p, Abc_Obj_t * pNode, Vec_Ptr_t *
     return Vec_StrArray( vFunc );
 }
 
+/**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.]
@@ -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)));
+        // construct the reset circuit and get the reset net feeding into it
-        assert( Abc_ObjIsBi(pNode) );
+        pNet = Io_MvParseAddResetCircuit( p, pName );
-        // 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 );
         // 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
+                assert( p->pResetLatch != NULL );
-                pNode = Abc_ObjFanin0(Abc_ObjFanin0(Abc_ObjFanin0(pNet)));
+                // construct the reset circuit and get the reset net feeding into it
-                assert( Abc_ObjIsBi(pNode) );
+                pNet = Io_MvParseAddResetCircuit( p, pName );
-                // 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 );
             }
-//            Io_ReadCreatePi( p->pNtk, pName );
+            // add the new PI node
-            Abc_ObjAddFanin( pNet, Abc_NtkCreatePi(p->pNtk) );
+//            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"

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;
 }
 

src/base/io/ioUtil.c

@@ -173,115 +173,44 @@ Abc_Ntk_t * Io_Read( char * pFileName, Io_FileType_t FileType, int fCheck )
         return NULL;
     if ( !Abc_NtkIsNetlist(pNtk) )
         return pNtk;
+    // 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 )
+    {
+        printf( "Hierarchy reader converted %d instances of blackboxes.\n", Abc_NtkBlackboxNum(pNtk) );
+        pNtk = Abc_NtkConvertBlackboxes( pTemp = pNtk );
+        Abc_NtkDelete( pTemp );
+        if ( pNtk == NULL )
+        {
+            fprintf( stdout, "Converting blackboxes has failed.\n" );
+            return NULL;
+        }
+    }
     // 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 );
-Abc_NtkPrintStats( stdout, pNtk, 0 );
+//    Io_WriteBlifMv( pNtk, "_temp_.mv" );
-/*
+        pNtk = Abc_NtkStrashBlifMv( pTemp = pNtk );
-{
-    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" );
+            fprintf( stdout, "Converting BLIF-MV to AIG has failed.\n" );
             return NULL;
         }
         return pNtk;
     }
-    // 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 )
-    {
-        printf( "Hierarchy reader converted %d instances of blackboxes.\n", Abc_NtkBlackboxNum(pNtk) );
-        pNtk = Abc_NtkConvertBlackboxes( pTemp = pNtk );
-        Abc_NtkDelete( pTemp );
-        if ( pNtk == NULL )
-        {
-            fprintf( stdout, "Converting blackboxes has failed.\n" );
-            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 )
-    {
-        printf( "Hierarchy reader converted %d instances of blackboxes.\n", Abc_NtkBlackboxNum(pNtk) );
-        pNtk = Abc_NtkConvertBlackboxes( pTemp = pNtk );
-        Abc_NtkDelete( pTemp );
-        if ( pNtk == NULL )
-        {
-            fprintf( stdout, "Converting blackboxes has failed.\n" );
-            return NULL;
-        }
-    }
     // convert the netlist into the logic network
     pNtk = Abc_NtkToLogic( pTemp = pNtk );
     Abc_NtkDelete( pTemp );
@@ -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 ( 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,59 +581,24 @@ 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 = Abc_NtkCreateNode( pNtk );   
-    pNode->pData = Abc_SopRegister( pNtk->pManFunc, "2\n1\n" );
+//    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.]

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 );

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 )

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" );
+        fprintf( stdout, "Io_WriteBlifMv(): 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" );
         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 " );

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" );

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                           ///
 ////////////////////////////////////////////////////////////////////////

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 )

src/bdd/cas/module.make

@@ -1,2 +1,3 @@
 SRC +=    src/bdd/cas/casCore.c \
-    src/bdd/cas/casDec
+    src/bdd/cas/casDec.c
+

src/map/if/if.h

@@ -47,6 +47,8 @@ extern "C" {
 #define IF_MAX_FUNC_LUTSIZE  15
 // a very large number
 #define IF_INFINITY          100000000  
+// the largest possible user cut cost
+#define IF_COST_MAX          ((1<<14)-1)
 
 // object types
 typedef enum { 
@@ -55,10 +57,7 @@ typedef enum {
     IF_CI,       // 2: combinational input
     IF_CO,       // 3: combinational output
     IF_AND,      // 4: AND node
-    IF_BI,       // 5: box input
+    IF_VOID      // 5: unused object
-    IF_BO,       // 6: box output
-    IF_BOX,      // 7: box
-    IF_VOID      // 8: unused object
 } If_Type_t;
 
 ////////////////////////////////////////////////////////////////////////
@@ -70,6 +69,7 @@ typedef struct If_Par_t_     If_Par_t;
 typedef struct If_Lib_t_     If_Lib_t;
 typedef struct If_Obj_t_     If_Obj_t;
 typedef struct If_Cut_t_     If_Cut_t;
+typedef struct If_Set_t_     If_Set_t;
 
 // parameters
 struct If_Par_t_
@@ -88,11 +88,13 @@ struct If_Par_t_
     int                fSeqMap;       // sequential mapping
     int                fVerbose;      // the verbosity flag
     // internal parameters
+    int                fAreaOnly;     // area only mode
     int                fTruth;        // truth table computation enabled
     int                fUsePerm;      // use permutation (delay info)
-    int                fUseBdds;      // sets local BDDs at the nodes
+    int                fUseBdds;      // use local BDDs as a cost function
-    int                fUseSops;      // sets local SOPs at the nodes
+    int                fUseSops;      // use local SOPs as a cost function
-    int                fUseCnfs;      // sets local CNFs at the nodes
+    int                fUseCnfs;      // use local CNFs as a cost function
+    int                fUseMv;        // use local MV-SOPs as a cost function
     int                nLatches;      // the number of latches in seq mapping
     int                fLiftLeaves;   // shift the leaves for seq mapping
     If_Lib_t *         pLutLib;       // the LUT library
@@ -129,11 +131,14 @@ struct If_Man_t_
     int                nLevelMax;     // the max number of AIG levels
     float              fEpsilon;      // epsilon used for comparison
     float              RequiredGlo;   // global required times
+    float              RequiredGlo2;  // global required times
     float              AreaGlo;       // global area
     int                nNets;         // the sum total of fanins of all LUTs in the mapping
     int                nCutsUsed;     // the number of cuts currently used
     int                nCutsMerged;   // the total number of cuts merged
     unsigned *         puTemp[4];     // used for the truth table computation
+    int                SortMode;      // one of the three sorting modes
+    int                fNextRound;    // set to 1 after the first round
     // sequential mapping
     Vec_Ptr_t *        vLatchOrder;   // topological ordering of latches
     Vec_Int_t *        vLags;         // sequentail lags of all nodes
@@ -141,15 +146,16 @@ struct If_Man_t_
     int                nMaxIters;     // the maximum number of iterations
     int                Period;        // the current value of the clock period (for seq mapping)
     // memory management
-    Mem_Fixed_t *      pMem;          // memory manager
+    int                nTruthWords;   // the size of the truth table if allocated
-    int                nEntrySize;    // the size of the entry
+    int                nPermWords;    // the size of the permutation array (in words)
-    int                nEntryBase;    // the size of the entry minus cut leaf arrays
+    int                nObjBytes;     // the size of the object
-    int                nTruthSize;    // the size of the truth table if allocated
+    int                nCutBytes;     // the size of the cut
-    int                nPermSize;     // the size of the permutation array (in words)
+    int                nSetBytes;     // the size of the cut set
-    int                nCutSize;      // the size of the cut
+    Mem_Fixed_t *      pMemObj;       // memory manager for objects (entrysize = nEntrySize)
-    // temporary cut storage
+    Mem_Fixed_t *      pMemSet;       // memory manager for sets of cuts (entrysize = nCutSize*(nCutsMax+1))
-    int                nCuts;         // the number of cuts used
+    If_Set_t *         pMemCi;        // memory for CI cutsets
-    If_Cut_t **        ppCuts;        // the storage space for cuts
+    If_Set_t *         pMemAnd;       // memory for AND cutsets
+    If_Set_t *         pFreeList;     // the list of free cutsets
 };
 
 // priority cut
@@ -169,6 +175,15 @@ struct If_Cut_t_
     unsigned *         pTruth;        // the truth table
 };
 
+// set of priority cut
+struct If_Set_t_
+{
+    short              nCutsMax;      // the max number of cuts
+    short              nCuts;         // the current number of cuts
+    If_Set_t *         pNext;         // next cutset in the free list
+    If_Cut_t **        ppCuts;        // the array of pointers to the cuts
+};
+
 // node extension
 struct If_Obj_t_
 {
@@ -182,36 +197,37 @@ struct If_Obj_t_
     unsigned           Level   : 22;  // logic level of the node
     int                Id;            // integer ID
     int                nRefs;         // the number of references
-    int                nCuts;         // the number of cuts
+    int                nVisits;       // the number of visits to this node
+    int                nVisitsCopy;   // the number of visits to this node
     If_Obj_t *         pFanin0;       // the first fanin 
     If_Obj_t *         pFanin1;       // the second fanin
     If_Obj_t *         pEquiv;        // the choice node
     float              EstRefs;       // estimated reference counter
     float              Required;      // required time of the onde
-    void *             pCopy;         // used for duplication
+    float              LValue;        // sequential arrival time of the node
-    If_Cut_t           Cuts[0];       // the cuts of the node
+    void *             pCopy;         // used for object duplication
+    If_Set_t *         pCutSet;       // the pointer to the cutset
+    If_Cut_t           CutBest;       // the best cut selected 
 };
 
-static inline If_Obj_t * If_ManConst1( If_Man_t * p )                        { return p->pConst1;                              }
-static inline If_Obj_t * If_ManCi( If_Man_t * p, int i )                     { return (If_Obj_t *)Vec_PtrEntry( p->vCis, i );  }
-static inline If_Obj_t * If_ManCo( If_Man_t * p, int i )                     { return (If_Obj_t *)Vec_PtrEntry( p->vCos, i );  }
-static inline If_Obj_t * If_ManObj( If_Man_t * p, int i )                    { return (If_Obj_t *)Vec_PtrEntry( p->vObjs, i ); }
-static inline If_Cut_t * If_ManCut( If_Man_t * p, int i )                    { return p->ppCuts[i];                            }
-
 static inline int        If_ManCiNum( If_Man_t * p )                         { return p->nObjs[IF_CI];               }
 static inline int        If_ManCoNum( If_Man_t * p )                         { return p->nObjs[IF_CO];               }
 static inline int        If_ManAndNum( If_Man_t * p )                        { return p->nObjs[IF_AND];              }
 static inline int        If_ManObjNum( If_Man_t * p )                        { return Vec_PtrSize(p->vObjs);         }
 
+static inline If_Obj_t * If_ManConst1( If_Man_t * p )                        { return p->pConst1;                              }
+static inline If_Obj_t * If_ManCi( If_Man_t * p, int i )                     { return (If_Obj_t *)Vec_PtrEntry( p->vCis, i );  }
+static inline If_Obj_t * If_ManCo( If_Man_t * p, int i )                     { return (If_Obj_t *)Vec_PtrEntry( p->vCos, i );  }
+static inline If_Obj_t * If_ManLi( If_Man_t * p, int i )                     { return (If_Obj_t *)Vec_PtrEntry( p->vCos, If_ManCoNum(p) - p->pPars->nLatches + i );  }
+static inline If_Obj_t * If_ManLo( If_Man_t * p, int i )                     { return (If_Obj_t *)Vec_PtrEntry( p->vCis, If_ManCiNum(p) - p->pPars->nLatches + i );  }
+static inline If_Obj_t * If_ManObj( If_Man_t * p, int i )                    { return (If_Obj_t *)Vec_PtrEntry( p->vObjs, i ); }
+
 static inline int        If_ObjIsConst1( If_Obj_t * pObj )                   { return pObj->Type == IF_CONST1;       }
 static inline int        If_ObjIsCi( If_Obj_t * pObj )                       { return pObj->Type == IF_CI;           }
 static inline int        If_ObjIsCo( If_Obj_t * pObj )                       { return pObj->Type == IF_CO;           }
 static inline int        If_ObjIsPi( If_Obj_t * pObj )                       { return If_ObjIsCi(pObj) && pObj->pFanin0 == NULL; }
 static inline int        If_ObjIsLatch( If_Obj_t * pObj )                    { return If_ObjIsCi(pObj) && pObj->pFanin0 != NULL; }
 static inline int        If_ObjIsAnd( If_Obj_t * pObj )                      { return pObj->Type == IF_AND;          }
-static inline int        If_ObjIsBi( If_Obj_t * pObj )                       { return pObj->Type == IF_BI;           }
-static inline int        If_ObjIsBo( If_Obj_t * pObj )                       { return pObj->Type == IF_BO;           }
-static inline int        If_ObjIsBox( If_Obj_t * pObj )                      { return pObj->Type == IF_BOX;          }
 
 static inline If_Obj_t * If_ObjFanin0( If_Obj_t * pObj )                     { return pObj->pFanin0;                 }
 static inline If_Obj_t * If_ObjFanin1( If_Obj_t * pObj )                     { return pObj->pFanin1;                 }
@@ -221,13 +237,14 @@ static inline void *     If_ObjCopy( If_Obj_t * pObj )                       { r
 static inline void       If_ObjSetCopy( If_Obj_t * pObj, void * pCopy )      { pObj->pCopy = pCopy;                  }
 static inline void       If_ObjSetChoice( If_Obj_t * pObj, If_Obj_t * pEqu ) { pObj->pEquiv = pEqu;                  }
 
-static inline If_Cut_t * If_ObjCut( If_Obj_t * pObj, int iCut )              { return pObj->Cuts + iCut;             }
+static inline If_Cut_t * If_ObjCutBest( If_Obj_t * pObj )                    { return &pObj->CutBest;                }
-static inline If_Cut_t * If_ObjCutTriv( If_Obj_t * pObj )                    { return pObj->Cuts;                    }
-static inline If_Cut_t * If_ObjCutBest( If_Obj_t * pObj )                    { return pObj->Cuts + (int)(pObj->nCuts > 1); }
 static inline unsigned   If_ObjCutSign( unsigned ObjId )                     { return (1 << (ObjId % 31));           }
 
-static inline float      If_ObjLValue( If_Obj_t * pObj )                     { return If_ObjCutTriv(pObj)->Delay;    }
+static inline float      If_ObjArrTime( If_Obj_t * pObj )                    { return If_ObjCutBest(pObj)->Delay;    }
-static inline void       If_ObjSetLValue( If_Obj_t * pObj, float LValue )    { If_ObjCutTriv(pObj)->Delay = LValue;  }
+static inline void       If_ObjSetArrTime( If_Obj_t * pObj, float ArrTime )  { If_ObjCutBest(pObj)->Delay = ArrTime; }
+
+static inline float      If_ObjLValue( If_Obj_t * pObj )                     { return pObj->LValue;                  }
+static inline void       If_ObjSetLValue( If_Obj_t * pObj, float LValue )    { pObj->LValue = LValue;                }
 
 static inline void *     If_CutData( If_Cut_t * pCut )                       { return *(void **)pCut;                }
 static inline void       If_CutSetData( If_Cut_t * pCut, void * pData )      { *(void **)pCut = pData;               }
@@ -264,20 +281,19 @@ static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { r
 #define If_ManForEachPo( p, pObj, i )                                          \
     Vec_PtrForEachEntryStop( p->vCos, pObj, i, If_ManCoNum(p) - p->pPars->nLatches )
 // iterator over the latches 
-#define If_ManForEachLatch( p, pObj, i )                                       \
+#define If_ManForEachLatchInput( p, pObj, i )                                  \
     Vec_PtrForEachEntryStart( p->vCos, pObj, i, If_ManCoNum(p) - p->pPars->nLatches )
+#define If_ManForEachLatchOutput( p, pObj, i )                                 \
+    Vec_PtrForEachEntryStart( p->vCis, pObj, i, If_ManCiNum(p) - p->pPars->nLatches )
 // iterator over all objects, including those currently not used
 #define If_ManForEachObj( p, pObj, i )                                         \
     Vec_PtrForEachEntry( p->vObjs, pObj, i )
-// iterator over logic nodes (AND and EXOR gates)
+// iterator over logic nodes 
 #define If_ManForEachNode( p, pObj, i )                                        \
     If_ManForEachObj( p, pObj, i ) if ( pObj->Type != IF_AND ) {} else
 // iterator over cuts of the node
 #define If_ObjForEachCut( pObj, pCut, i )                                      \
-    for ( i = 0; (i < (int)(pObj)->nCuts) && ((pCut) = (pObj)->Cuts + i); i++ )
+    for ( i = 0; (i < (pObj)->pCutSet->nCuts) && ((pCut) = (pObj)->pCutSet->ppCuts[i]); i++ )
-// iterator over cuts of the node
-#define If_ObjForEachCutStart( pObj, pCut, i, Start )                          \
-    for ( i = Start; (i < (int)(pObj)->nCuts) && ((pCut) = (pObj)->Cuts + i); i++ )
 // iterator over the leaves of the cut
 #define If_CutForEachLeaf( p, pCut, pLeaf, i )                                 \
     for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, (pCut)->pLeaves[i])); i++ )
@@ -295,6 +311,7 @@ static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { r
 
 /*=== ifCore.c ===========================================================*/
 extern int             If_ManPerformMapping( If_Man_t * p );
+extern int             If_ManPerformMappingComb( If_Man_t * p );
 /*=== ifCut.c ============================================================*/
 extern float           If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut, int nLevels );
 extern float           If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut, int nLevels );
@@ -304,10 +321,11 @@ extern void            If_CutPrint( If_Man_t * p, If_Cut_t * pCut );
 extern void            If_CutPrintTiming( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutFlow( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutAverageRefs( If_Man_t * p, If_Cut_t * pCut );
-extern int             If_CutFilter( If_Man_t * p, If_Cut_t * pCut );
+extern int             If_CutFilter( If_Set_t * pCutSet, If_Cut_t * pCut );
+extern void            If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut );
 extern int             If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut );
 extern void            If_CutLift( If_Cut_t * pCut );
-extern void            If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc );
+extern void            If_CutCopy( If_Man_t * p, If_Cut_t * pCutDest, If_Cut_t * pCutSrc );
 extern void            If_ManSortCuts( If_Man_t * p, int Mode );
 /*=== ifMan.c =============================================================*/
 extern If_Man_t *      If_ManStart( If_Par_t * pPars );
@@ -316,12 +334,16 @@ extern If_Obj_t *      If_ManCreateCi( If_Man_t * p );
 extern If_Obj_t *      If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 );
 extern If_Obj_t *      If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_t * pFan1, int fCompl1 );
 extern void            If_ManCreateChoice( If_Man_t * p, If_Obj_t * pRepr );
+extern void            If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId );
+extern void            If_ManSetupCiCutSets( If_Man_t * p );
+extern If_Set_t *      If_ManSetupNodeCutSet( If_Man_t * p, If_Obj_t * pObj );
+extern void            If_ManDerefNodeCutSet( If_Man_t * p, If_Obj_t * pObj );
+extern void            If_ManDerefChoiceCutSet( If_Man_t * p, If_Obj_t * pObj );
+extern void            If_ManSetupSetAll( If_Man_t * p );
 /*=== ifMap.c =============================================================*/
-extern void            If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode );
+extern void            If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPreprocess );
-extern void            If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode );
+extern void            If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPreprocess );
-extern int             If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fRequired, char * pLabel );
+extern int             If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPreprocess, char * pLabel );
-/*=== ifPrepro.c ==========================================================*/
-extern void            If_ManPerformMappingPreprocess( If_Man_t * p );
 /*=== ifReduce.c ==========================================================*/
 extern void            If_ManImproveMapping( If_Man_t * p );
 /*=== ifSeq.c =============================================================*/
@@ -336,9 +358,11 @@ extern void            If_ManCleanNodeCopy( If_Man_t * p );
 extern void            If_ManCleanCutData( If_Man_t * p );
 extern void            If_ManCleanMarkV( If_Man_t * p );
 extern float           If_ManDelayMax( If_Man_t * p, int fSeq );
-extern void            If_ManComputeRequired( If_Man_t * p, int fFirstTime );
+extern void            If_ManComputeRequired( If_Man_t * p );
 extern float           If_ManScanMapping( If_Man_t * p );
 extern float           If_ManScanMappingSeq( If_Man_t * p );
+extern void            If_ManResetOriginalRefs( If_Man_t * p );
+extern int             If_ManCrossCut( If_Man_t * p );
 
 #ifdef __cplusplus
 }

src/map/if/ifCore.c

@@ -41,54 +41,98 @@
 ***********************************************************************/
 int If_ManPerformMapping( If_Man_t * p )
 {
-    If_Obj_t * pObj;
+    p->pPars->fAreaOnly = p->pPars->fArea; // temporary
-    int clkTotal = clock();
+
-    int RetValue, i;
+    // create the CI cutsets
+    If_ManSetupCiCutSets( p );
+    // allocate memory for other cutsets
+    If_ManSetupSetAll( p );
 
     // try sequential mapping
     if ( p->pPars->fSeqMap )
     {
+        int RetValue;
+//        printf( "Currently sequential mapping is not performed.\n" );
         RetValue = If_ManPerformMappingSeq( p );
-        if ( p->pPars->fVerbose )
-        {
-            PRT( "Total time", clock() - clkTotal );
-        }
         return RetValue;
+//        return 1;
     }
 
-    // set arrival times and trivial cuts at const 1 and PIs
+    return If_ManPerformMappingComb( p );
-    If_ManConst1(p)->Cuts[0].Delay = 0.0;
+}
-    If_ManForEachCi( p, pObj, i )
+
-        pObj->Cuts[0].Delay = p->pPars->pTimesArr[i];
+
-    // set the fanout estimates of the PIs
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManPerformMappingComb( If_Man_t * p )
+{
+    If_Obj_t * pObj;
+    int clkTotal = clock();
+    int i;
+
+    // set arrival times and fanout estimates
     If_ManForEachCi( p, pObj, i )
+    {
+        If_ObjSetArrTime( pObj, p->pPars->pTimesArr[i] );
         pObj->EstRefs = (float)1.0;
+    }
+
     // delay oriented mapping
-    if ( p->pPars->fPreprocess && !p->pPars->fArea && p->pPars->nCutsMax >= 4  )
+    if ( p->pPars->fPreprocess && !p->pPars->fArea )
-        If_ManPerformMappingPreprocess( p );
+    {
-    else
+        // map for delay
         If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 1, "Delay" );
+        // map for delay second option
+        p->pPars->fFancy = 1;
+        If_ManResetOriginalRefs( p );
+        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 1, "Delay-2" );
+        p->pPars->fFancy = 0;
+        // map for area
+        p->pPars->fArea = 1;
+        If_ManResetOriginalRefs( p );
+        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 1, "Area" );
+        p->pPars->fArea = 0;
+    }
+    else
+        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 0, "Delay" );
+
     // try to improve area by expanding and reducing the cuts
     if ( p->pPars->fExpRed && !p->pPars->fTruth )
         If_ManImproveMapping( p );
+
     // area flow oriented mapping
     for ( i = 0; i < p->pPars->nFlowIters; i++ )
     {
-        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 1, 1, "Flow" );
+        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 1, 0, "Flow" );
         if ( p->pPars->fExpRed && !p->pPars->fTruth )
             If_ManImproveMapping( p );
     }
+
     // area oriented mapping
     for ( i = 0; i < p->pPars->nAreaIters; i++ )
     {
-        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 2, 1, "Area" );
+        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 2, 0, "Area" );
         if ( p->pPars->fExpRed && !p->pPars->fTruth )
             If_ManImproveMapping( p );
     }
+
     if ( p->pPars->fVerbose )
     {
+//        printf( "Total memory = %7.2f Mb. Peak cut memory = %7.2f Mb.  ", 
+//            1.0 * (p->nObjBytes + 2*sizeof(void *)) * If_ManObjNum(p) / (1<<20), 
+//            1.0 * p->nSetBytes * Mem_FixedReadMaxEntriesUsed(p->pMemSet) / (1<<20) );
         PRT( "Total time", clock() - clkTotal );
     }
+//    printf( "Cross cut memory = %d.\n", Mem_FixedReadMaxEntriesUsed(p->pMemSet) );
     return 1;
 }
 

src/map/if/ifCut.c

@@ -87,13 +87,14 @@ static inline int If_CutCheckEquality( If_Cut_t * pDom, If_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-int If_CutFilter( If_Man_t * p, If_Cut_t * pCut )
+int If_CutFilter( If_Set_t * pCutSet, If_Cut_t * pCut )
 { 
     If_Cut_t * pTemp;
-    int i;
+    int i, k;
-    for ( i = 0; i < p->nCuts; i++ )
+    assert( pCutSet->ppCuts[pCutSet->nCuts] == pCut );
+    for ( i = 0; i < pCutSet->nCuts; i++ )
     {
-        pTemp = p->ppCuts[i];
+        pTemp = pCutSet->ppCuts[i];
         if ( pTemp->nLeaves > pCut->nLeaves )
         {
             // do not fiter the first cut
@@ -105,10 +106,15 @@ int If_CutFilter( If_Man_t * p, If_Cut_t * pCut )
             // check containment seriously
             if ( If_CutCheckDominance( pCut, pTemp ) )
             {
-                // removed contained cut
+//                p->ppCuts[i] = p->ppCuts[p->nCuts-1];
-                p->ppCuts[i] = p->ppCuts[p->nCuts-1];
+//                p->ppCuts[p->nCuts-1] = pTemp;
-                p->ppCuts[p->nCuts-1] = pTemp;
+//                p->nCuts--;
-                p->nCuts--;
+//                i--;
+                // remove contained cut
+                for ( k = i; k < pCutSet->nCuts; k++ )
+                    pCutSet->ppCuts[k] = pCutSet->ppCuts[k+1];
+                pCutSet->ppCuts[pCutSet->nCuts] = pTemp;
+                pCutSet->nCuts--;
                 i--;
             }
          }
@@ -290,6 +296,7 @@ int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut )
         if ( !If_CutMergeOrdered( pCut0, pCut1, pCut ) )
             return 0;
     }
+    pCut->uSign = pCut0->uSign | pCut1->uSign;
     return 1;
 }
 
@@ -400,6 +407,7 @@ int If_CutCompareArea( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
 ***********************************************************************/
 void If_ManSortCuts( If_Man_t * p, int Mode )
 {
+/*
     // sort the cuts
     if ( Mode || p->pPars->fArea ) // area
         qsort( p->ppCuts, p->nCuts, sizeof(If_Cut_t *), (int (*)(const void *, const void *))If_CutCompareArea );
@@ -407,6 +415,115 @@ void If_ManSortCuts( If_Man_t * p, int Mode )
         qsort( p->ppCuts, p->nCuts, sizeof(If_Cut_t *), (int (*)(const void *, const void *))If_CutCompareDelayOld );
     else
         qsort( p->ppCuts, p->nCuts, sizeof(If_Cut_t *), (int (*)(const void *, const void *))If_CutCompareDelay );
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison function for two cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int If_ManSortCompare( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC1 )
+{
+    if ( p->SortMode == 1 ) // area
+    {
+        if ( pC0->Area < pC1->Area - 0.0001 )
+            return -1;
+        if ( pC0->Area > pC1->Area + 0.0001 )
+            return 1;
+        if ( pC0->AveRefs > pC1->AveRefs )
+            return -1;
+        if ( pC0->AveRefs < pC1->AveRefs )
+            return 1;
+        if ( pC0->nLeaves < pC1->nLeaves )
+            return -1;
+        if ( pC0->nLeaves > pC1->nLeaves )
+            return 1;
+        if ( pC0->Delay < pC1->Delay - 0.0001 )
+            return -1;
+        if ( pC0->Delay > pC1->Delay + 0.0001 )
+            return 1;
+        return 0;
+    }
+    if ( p->SortMode == 0 ) // delay
+    {
+        if ( pC0->Delay < pC1->Delay - 0.0001 )
+            return -1;
+        if ( pC0->Delay > pC1->Delay + 0.0001 )
+            return 1;
+        if ( pC0->nLeaves < pC1->nLeaves )
+            return -1;
+        if ( pC0->nLeaves > pC1->nLeaves )
+            return 1;
+        if ( pC0->Area < pC1->Area - 0.0001 )
+            return -1;
+        if ( pC0->Area > pC1->Area + 0.0001 )
+            return 1;
+        return 0;
+    }
+    assert( p->SortMode == 2 ); // delay old
+    if ( pC0->Delay < pC1->Delay - 0.0001 )
+        return -1;
+    if ( pC0->Delay > pC1->Delay + 0.0001 )
+        return 1;
+    if ( pC0->Area < pC1->Area - 0.0001 )
+        return -1;
+    if ( pC0->Area > pC1->Area + 0.0001 )
+        return 1;
+    if ( pC0->nLeaves < pC1->nLeaves )
+        return -1;
+    if ( pC0->nLeaves > pC1->nLeaves )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs incremental sorting of cuts.]
+
+  Description [Currently only the trivial sorting is implemented.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut )
+{
+//    int Counter = 0;
+    int i;
+
+    // the new cut is the last one
+    assert( pCutSet->ppCuts[pCutSet->nCuts] == pCut );
+    assert( pCutSet->nCuts <= pCutSet->nCutsMax );
+
+    // cut structure is empty
+    if ( pCutSet->nCuts == 0 )
+    {
+        pCutSet->nCuts++;
+        return;
+    }
+
+    // the cut will be added - find its place
+    for ( i = pCutSet->nCuts-1; i >= 0; i-- )
+    {
+//        Counter++;
+        if ( If_ManSortCompare( p, pCutSet->ppCuts[i], pCut ) <= 0 )
+            break;
+        pCutSet->ppCuts[i+1] = pCutSet->ppCuts[i];
+        pCutSet->ppCuts[i] = pCut;
+    }
+//    printf( "%d ", Counter );
+
+    // update the number of cuts
+    if ( pCutSet->nCuts < pCutSet->nCutsMax )
+        pCutSet->nCuts++;
 }
 
 /**Function*************************************************************
@@ -635,7 +752,7 @@ void If_CutLift( If_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-void If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc )
+void If_CutCopy( If_Man_t * p, If_Cut_t * pCutDest, If_Cut_t * pCutSrc )
 {
     int * pLeaves;
     char * pPerm;
@@ -645,17 +762,11 @@ void If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc )
     pPerm   = pCutDest->pPerm;
     pTruth  = pCutDest->pTruth;
     // copy the cut info
-    *pCutDest = *pCutSrc;
+    memcpy( pCutDest, pCutSrc, p->nCutBytes );
     // restore the arrays
     pCutDest->pLeaves = pLeaves;
     pCutDest->pPerm   = pPerm;
     pCutDest->pTruth  = pTruth;
-    // copy the array data
-    memcpy( pCutDest->pLeaves, pCutSrc->pLeaves, sizeof(int) * pCutSrc->nLeaves );
-    if ( pCutSrc->pPerm )
-        memcpy( pCutDest->pPerm, pCutSrc->pPerm, sizeof(unsigned) * If_CutPermWords(pCutSrc->nLimit) );
-    if ( pCutSrc->pTruth )
-        memcpy( pCutDest->pTruth, pCutSrc->pTruth, sizeof(unsigned) * If_CutTruthWords(pCutSrc->nLimit) );
 }
 
 ////////////////////////////////////////////////////////////////////////

src/map/if/ifMan.c

@@ -25,7 +25,9 @@
 ////////////////////////////////////////////////////////////////////////
 
 static If_Obj_t * If_ManSetupObj( If_Man_t * p );
-static If_Cut_t ** If_ManSetupCuts( If_Man_t * p );
+
+static void       If_ManCutSetRecycle( If_Man_t * p, If_Set_t * pSet ) { pSet->pNext = p->pFreeList; p->pFreeList = pSet;                            }
+static If_Set_t * If_ManCutSetFetch( If_Man_t * p )                    { If_Set_t * pTemp = p->pFreeList; p->pFreeList = p->pFreeList->pNext; return pTemp; }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -57,27 +59,26 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
     p->vMapped = Vec_PtrAlloc( 100 );
     p->vTemp   = Vec_PtrAlloc( 100 );
     // prepare the memory manager
-    p->nTruthSize = p->pPars->fTruth? If_CutTruthWords( p->pPars->nLutSize ) : 0;
+    p->nTruthWords = p->pPars->fTruth? If_CutTruthWords( p->pPars->nLutSize ) : 0;
-    p->nPermSize  = p->pPars->fUsePerm? If_CutPermWords( p->pPars->nLutSize ) : 0;
+    p->nPermWords  = p->pPars->fUsePerm? If_CutPermWords( p->pPars->nLutSize ) : 0;
-    p->nCutSize   = sizeof(If_Cut_t) + sizeof(int) * (p->pPars->nLutSize + p->nPermSize + p->nTruthSize);
+    p->nObjBytes   = sizeof(If_Obj_t) + sizeof(int) * (p->pPars->nLutSize + p->nPermWords + p->nTruthWords);
-    p->nEntrySize = sizeof(If_Obj_t) + p->pPars->nCutsMax * p->nCutSize;
+    p->nCutBytes   = sizeof(If_Cut_t) + sizeof(int) * (p->pPars->nLutSize + p->nPermWords + p->nTruthWords);
-    p->nEntryBase = sizeof(If_Obj_t) + p->pPars->nCutsMax * sizeof(If_Cut_t);
+    p->nSetBytes   = sizeof(If_Set_t) + (sizeof(If_Cut_t *) + p->nCutBytes) * (p->pPars->nCutsMax + 1);
-    p->pMem = Mem_FixedStart( p->nEntrySize );
+    p->pMemObj     = Mem_FixedStart( p->nObjBytes );
+//    p->pMemSet     = Mem_FixedStart( p->nSetBytes );
     // report expected memory usage
     if ( p->pPars->fVerbose )
-        printf( "Memory (bytes): Truth = %3d. Cut = %3d. Entry = %4d. Total = %.2f Mb / 1K AIG nodes\n", 
+        printf( "Memory (bytes): Truth = %4d. Cut = %4d. Obj = %4d. Set = %4d.\n", 
-            4 * p->nTruthSize, p->nCutSize, p->nEntrySize, 1000.0 * p->nEntrySize / (1<<20) );
+            4 * p->nTruthWords, p->nCutBytes, p->nObjBytes, p->nSetBytes );
     // room for temporary truth tables
-    p->puTemp[0] = p->pPars->fTruth? ALLOC( unsigned, 4 * p->nTruthSize ) : NULL;
+    p->puTemp[0] = p->pPars->fTruth? ALLOC( unsigned, 4 * p->nTruthWords ) : NULL;
-    p->puTemp[1] = p->puTemp[0] + p->nTruthSize;
+    p->puTemp[1] = p->puTemp[0] + p->nTruthWords;
-    p->puTemp[2] = p->puTemp[1] + p->nTruthSize;
+    p->puTemp[2] = p->puTemp[1] + p->nTruthWords;
-    p->puTemp[3] = p->puTemp[2] + p->nTruthSize;
+    p->puTemp[3] = p->puTemp[2] + p->nTruthWords;
     // create the constant node
     p->pConst1 = If_ManSetupObj( p );
     p->pConst1->Type = IF_CONST1;
     p->pConst1->fPhase = 1;
-    // create temporary cuts
-    p->ppCuts = If_ManSetupCuts( p );
     return p;
 }
 
@@ -94,8 +95,6 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
 ***********************************************************************/
 void If_ManStop( If_Man_t * p )
 {
-    If_Cut_t * pTemp;
-    int i;
     Vec_PtrFree( p->vCis );
     Vec_PtrFree( p->vCos );
     Vec_PtrFree( p->vObjs );
@@ -103,20 +102,16 @@ void If_ManStop( If_Man_t * p )
     Vec_PtrFree( p->vTemp );
     if ( p->vLatchOrder ) Vec_PtrFree( p->vLatchOrder );
     if ( p->vLags ) Vec_IntFree( p->vLags );
-    Mem_FixedStop( p->pMem, 0 );
+    Mem_FixedStop( p->pMemObj, 0 );
+//    Mem_FixedStop( p->pMemSet, 0 );
+    FREE( p->pMemCi );
+    FREE( p->pMemAnd );
+    FREE( p->puTemp[0] );
     // free pars memory
     if ( p->pPars->pTimesArr )
         FREE( p->pPars->pTimesArr );
     if ( p->pPars->pTimesReq )
         FREE( p->pPars->pTimesReq );
-    // free temporary cut memory
-    pTemp = p->ppCuts[0];
-    for ( i = 1; i < 1 + p->pPars->nCutsMax * p->pPars->nCutsMax; i++ )
-        if ( pTemp > p->ppCuts[i] )
-            pTemp = p->ppCuts[i];
-    FREE( p->puTemp[0] );
-    free( pTemp );
-    free( p->ppCuts );
     free( p );
 }
 
@@ -183,8 +178,8 @@ If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_
     pObj->Type    = IF_AND;
     pObj->fCompl0 = fCompl0;
     pObj->fCompl1 = fCompl1;
-    pObj->pFanin0 = pFan0; pFan0->nRefs++;
+    pObj->pFanin0 = pFan0; pFan0->nRefs++; pFan0->nVisits++; pFan0->nVisitsCopy++;
-    pObj->pFanin1 = pFan1; pFan1->nRefs++;
+    pObj->pFanin1 = pFan1; pFan1->nRefs++; pFan1->nVisits++; pFan1->nVisitsCopy++;
     pObj->fPhase  = (fCompl0 ^ pFan0->fPhase) & (fCompl1 ^ pFan1->fPhase);
     pObj->Level   = 1 + IF_MAX( pFan0->Level, pFan1->Level );
     if ( p->nLevelMax < (int)pObj->Level )
@@ -211,13 +206,94 @@ void If_ManCreateChoice( If_Man_t * p, If_Obj_t * pObj )
     assert( pObj->fRepr == 0 );
     pObj->fRepr = 1;
     // update the level of this node (needed for correct required time computation)
-    for ( pTemp = pObj->pEquiv; pTemp; pTemp = pTemp->pEquiv )
+    for ( pTemp = pObj; pTemp; pTemp = pTemp->pEquiv )
+    {
         pObj->Level = IF_MAX( pObj->Level, pTemp->Level );
+        pTemp->nVisits++; pTemp->nVisitsCopy++;
+    }
     // mark the largest level
     if ( p->nLevelMax < (int)pObj->Level )
         p->nLevelMax = (int)pObj->Level;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prepares memory for one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManSetupCut( If_Man_t * p, If_Cut_t * pCut )
+{
+    memset( pCut, 0, sizeof(If_Cut_t) );
+    pCut->nLimit  = p->pPars->nLutSize;
+    pCut->pLeaves = (int *)(pCut + 1);
+    if ( p->pPars->fUsePerm )
+        pCut->pPerm  = (char *)(pCut->pLeaves + p->pPars->nLutSize);
+    if ( p->pPars->fTruth )
+        pCut->pTruth = pCut->pLeaves + p->pPars->nLutSize + p->nPermWords;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares memory for one cutset.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManSetupSet( If_Man_t * p, If_Set_t * pSet )
+{
+    char * pArray;
+    int i;
+    pSet->nCuts = 0;
+    pSet->nCutsMax = p->pPars->nCutsMax;
+    pSet->ppCuts = (If_Cut_t **)(pSet + 1);
+    pArray = (char *)pSet->ppCuts + sizeof(If_Cut_t *) * (pSet->nCutsMax+1);
+    for ( i = 0; i <= pSet->nCutsMax; i++ )
+    {
+        pSet->ppCuts[i] = (If_Cut_t *)(pArray + i * p->nCutBytes); 
+        If_ManSetupCut( p, pSet->ppCuts[i] );
+    }
+//    pArray += (pSet->nCutsMax + 1) * p->nCutBytes;
+//    assert( ((char *)pArray) - ((char *)pSet) == p->nSetBytes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares memory for one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId )
+{
+    pCut->fCompl     = 0;
+    pCut->nLimit     = p->pPars->nLutSize;
+    pCut->nLeaves    = 1;
+    pCut->pLeaves[0] = p->pPars->fLiftLeaves? (ObjId << 8) : ObjId;
+    pCut->uSign      = If_ObjCutSign( pCut->pLeaves[0] );
+    // set up elementary truth table of the unit cut
+    if ( p->pPars->fTruth )
+    {
+        int i, nTruthWords;
+        nTruthWords = Extra_TruthWordNum( pCut->nLimit );
+        for ( i = 0; i < nTruthWords; i++ )
+            If_CutTruth(pCut)[i] = 0xAAAAAAAA;
+    }
+}
+
 /**Function*************************************************************
 
   Synopsis    [Prepares memory for the node with cuts.]
@@ -231,47 +307,22 @@ void If_ManCreateChoice( If_Man_t * p, If_Obj_t * pObj )
 ***********************************************************************/
 If_Obj_t * If_ManSetupObj( If_Man_t * p )
 {
-    If_Cut_t * pCut;
     If_Obj_t * pObj;
-    int i, * pArrays, nTruthWords;
     // get memory for the object
-    pObj = (If_Obj_t *)Mem_FixedEntryFetch( p->pMem );
+    pObj = (If_Obj_t *)Mem_FixedEntryFetch( p->pMemObj );
-    memset( pObj, 0, p->nEntryBase );
+    memset( pObj, 0, sizeof(If_Obj_t) );
-    // organize memory
+    If_ManSetupCut( p, &pObj->CutBest );
-    pArrays = (int *)((char *)pObj + p->nEntryBase);
-    for ( i = 0; i < p->pPars->nCutsMax; i++ )
-    {
-        pCut = pObj->Cuts + i;
-        pCut->nLimit  = p->pPars->nLutSize;
-        pCut->pLeaves = pArrays + i * p->pPars->nLutSize;
-        pCut->pPerm   = (char *)(p->pPars->fUsePerm? pArrays + p->pPars->nCutsMax * p->pPars->nLutSize + i * p->nPermSize : NULL);
-        pCut->pTruth  = p->pPars->fTruth? pArrays + p->pPars->nCutsMax * (p->pPars->nLutSize + p->nPermSize) + i * p->nTruthSize : NULL;
-    }
     // assign ID and save 
     pObj->Id = Vec_PtrSize(p->vObjs);
     Vec_PtrPush( p->vObjs, pObj );
-    // assign elementary cut
-    pCut = pObj->Cuts;
-    pCut->nLeaves    = 1;
-    pCut->pLeaves[0] = p->pPars->fLiftLeaves? (pObj->Id << 8) : pObj->Id;
-    pCut->uSign      = If_ObjCutSign( pCut->pLeaves[0] );
-    // set the number of cuts
-    pObj->nCuts = 1;
     // set the required times
     pObj->Required = IF_FLOAT_LARGE;
-    // set up elementary truth table of the unit cut
-    if ( p->pPars->fTruth )
-    {
-        nTruthWords = Extra_TruthWordNum( pCut->nLimit );
-        for ( i = 0; i < nTruthWords; i++ )
-            If_CutTruth(pCut)[i] = 0xAAAAAAAA;
-    }
     return pObj;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Prepares memory for additional cuts of the manager.]
+  Synopsis    [Prepares memory for one cut.]
 
   Description []
                
@@ -280,31 +331,162 @@ If_Obj_t * If_ManSetupObj( If_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-If_Cut_t ** If_ManSetupCuts( If_Man_t * p )
+void If_ManSetupCiCutSets( If_Man_t * p )
 {
-    If_Cut_t ** pCutStore;
+    If_Obj_t * pObj;
-    int * pArrays, nCutsTotal, i;
+    int i;
-    // decide how many cuts to alloc
+    assert( p->pMemCi == NULL );
-    nCutsTotal = 1 + p->pPars->nCutsMax * p->pPars->nCutsMax;
+    // create elementary cuts for the CIs
-    // allocate and clean space for cuts
+    If_ManForEachCi( p, pObj, i )
-    pCutStore = (If_Cut_t **)ALLOC( If_Cut_t *, (nCutsTotal + 1) );
+        If_ManSetupCutTriv( p, &pObj->CutBest, pObj->Id );
-    memset( pCutStore, 0, sizeof(If_Cut_t *) * (nCutsTotal + 1) );
+    // create elementary cutsets for the CIs
-    pCutStore[0] = (If_Cut_t *)ALLOC( char, p->nCutSize * nCutsTotal );
+    p->pMemCi = (If_Set_t *)malloc( If_ManCiNum(p) * (sizeof(If_Set_t) + sizeof(void *)) );
-    memset( pCutStore[0], 0, p->nCutSize * nCutsTotal );
+    If_ManForEachCi( p, pObj, i )
-    // assign cut paramters and space for the cut leaves
-    assert( sizeof(int) == sizeof(unsigned) );
-    pArrays = (int *)((char *)pCutStore[0] + sizeof(If_Cut_t) * nCutsTotal);
-    for ( i = 0; i < nCutsTotal; i++ )
     {
-        pCutStore[i] = (If_Cut_t *)((char *)pCutStore[0] + sizeof(If_Cut_t) * i);
+        pObj->pCutSet = (If_Set_t *)((char *)p->pMemCi + i * (sizeof(If_Set_t) + sizeof(void *)));
-        pCutStore[i]->nLimit  = p->pPars->nLutSize;
+        pObj->pCutSet->nCuts = 1;
-        pCutStore[i]->pLeaves = pArrays + i * p->pPars->nLutSize;
+        pObj->pCutSet->nCutsMax = p->pPars->nCutsMax;
-        pCutStore[i]->pPerm   = (char *)(p->pPars->fUsePerm? pArrays + nCutsTotal * p->pPars->nLutSize + i * p->nPermSize : NULL);
+        pObj->pCutSet->ppCuts = (If_Cut_t **)(pObj->pCutSet + 1);
-        pCutStore[i]->pTruth  = p->pPars->fTruth? pArrays + nCutsTotal * (p->pPars->nLutSize + p->nPermSize) + i * p->nTruthSize : NULL;
+        pObj->pCutSet->ppCuts[0] = &pObj->CutBest;
     }
-    return pCutStore;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prepares cutset of the node.]
+
+  Description [Elementary cutset will be added last.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Set_t * If_ManSetupNodeCutSet( If_Man_t * p, If_Obj_t * pObj )
+{
+    assert( If_ObjIsAnd(pObj) );
+    assert( pObj->pCutSet == NULL );
+//    pObj->pCutSet = (If_Set_t *)Mem_FixedEntryFetch( p->pMemSet );
+//    If_ManSetupSet( p, pObj->pCutSet );
+
+    pObj->pCutSet = If_ManCutSetFetch( p );
+    pObj->pCutSet->nCuts = 0;
+    pObj->pCutSet->nCutsMax = p->pPars->nCutsMax;
+
+    return pObj->pCutSet;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dereferences cutset of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManDerefNodeCutSet( If_Man_t * p, If_Obj_t * pObj )
+{
+    If_Obj_t * pFanin;
+    assert( If_ObjIsAnd(pObj) );
+    // consider the node
+    assert( pObj->nVisits >= 0 );
+    if ( pObj->nVisits == 0 )
+    {
+//        Mem_FixedEntryRecycle( p->pMemSet, (char *)pObj->pCutSet );
+        If_ManCutSetRecycle( p, pObj->pCutSet );
+        pObj->pCutSet = NULL;
+    }
+    // consider the first fanin
+    pFanin = If_ObjFanin0(pObj);
+    assert( pFanin->nVisits > 0 );
+    if ( !If_ObjIsCi(pFanin) && --pFanin->nVisits == 0 )
+    {
+//        Mem_FixedEntryRecycle( p->pMemSet, (char *)pFanin->pCutSet );
+        If_ManCutSetRecycle( p, pFanin->pCutSet );
+        pFanin->pCutSet = NULL;
+    }
+    // consider the second fanin
+    pFanin = If_ObjFanin1(pObj);
+    assert( pFanin->nVisits > 0 );
+    if ( !If_ObjIsCi(pFanin) && --pFanin->nVisits == 0 )
+    {
+//        Mem_FixedEntryRecycle( p->pMemSet, (char *)pFanin->pCutSet );
+        If_ManCutSetRecycle( p, pFanin->pCutSet );
+        pFanin->pCutSet = NULL;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dereferences cutset of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManDerefChoiceCutSet( If_Man_t * p, If_Obj_t * pObj )
+{
+    If_Obj_t * pTemp;
+    assert( If_ObjIsAnd(pObj) );
+    assert( pObj->fRepr );
+    assert( pObj->nVisits > 0 );
+    // consider the nodes in the choice class
+    for ( pTemp = pObj; pTemp; pTemp = pTemp->pEquiv )
+    {
+        assert( pTemp == pObj || pTemp->nVisits == 1 );
+        if ( --pTemp->nVisits == 0 )
+        {
+//            Mem_FixedEntryRecycle( p->pMemSet, (char *)pTemp->pCutSet );
+            If_ManCutSetRecycle( p, pTemp->pCutSet );
+            pTemp->pCutSet = NULL;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dereferences cutset of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManSetupSetAll( If_Man_t * p )
+{
+    If_Set_t * pCutSet;
+    int i, nCrossCut, nCutSets;
+    nCrossCut = If_ManCrossCut( p );
+    nCutSets = 128 + nCrossCut;
+    p->pFreeList = p->pMemAnd = pCutSet = (If_Set_t *)malloc( nCutSets * p->nSetBytes );
+    for ( i = 0; i < nCutSets; i++ )
+    {
+        If_ManSetupSet( p, pCutSet );
+        if ( i == nCutSets - 1 )
+            pCutSet->pNext = NULL;
+        else
+            pCutSet->pNext = (If_Set_t *)( (char *)pCutSet + p->nSetBytes );
+        pCutSet = pCutSet->pNext;
+    }
+    assert( pCutSet == NULL );
+
+    if ( p->pPars->fVerbose )
+    {
+        printf( "Total memory = %7.2f Mb. Peak cut memory = %7.2f Mb.  \n", 
+            1.0 * (p->nObjBytes + 2*sizeof(void *)) * If_ManObjNum(p) / (1<<20), 
+            1.0 * p->nSetBytes * nCrossCut / (1<<20) );
+    }
+//    printf( "Cross cut = %d.\n", nCrossCut );
+
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/map/if/ifMap.c

@@ -24,16 +24,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-/*
-  Ideas to try:
-  - reverse order of area recovery
-  - ordering of the outputs by size
-  - merging Delay, Delay2, and Area
-  - expand/reduce area recovery
-  - use average nrefs for tie-breaking
-
-*/
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -69,13 +59,14 @@ static inline int If_WordCountOnes( unsigned uWord )
   SeeAlso     []
 
 ***********************************************************************/
-void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode )
+void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPreprocess )
 {
+    If_Set_t * pCutSet;
     If_Cut_t * pCut0, * pCut1, * pCut;
-    int i, k, iCut;
+    int i, k;
 
-    assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->nCuts > 1 );
+    assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->pCutSet->nCuts > 1 );
-    assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->nCuts > 1 );
+    assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->pCutSet->nCuts > 1 );
 
     // prepare
     if ( !p->pPars->fSeqMap )
@@ -88,40 +79,41 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode )
     if ( Mode && pObj->nRefs > 0 )
         If_CutDeref( p, If_ObjCutBest(pObj), IF_INFINITY );
 
-    // save the best cut as one of the candidate cuts
+    // prepare the cutset
-    p->nCuts = 0;
+    pCutSet = If_ManSetupNodeCutSet( p, pObj );
-    p->nCutsMerged++;
+
-    if ( Mode )
+    // get the current assigned best cut
+    pCut = If_ObjCutBest(pObj);
+    if ( pCut->nLeaves > 0 )
     {
         // recompute the parameters of the best cut
-        pCut = If_ObjCutBest(pObj);
         pCut->Delay = If_CutDelay( p, pCut );
         assert( pCut->Delay <= pObj->Required + p->fEpsilon );
         pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, IF_INFINITY ) : If_CutFlow( p, pCut );
         // save the best cut from the previous iteration
-        If_CutCopy( p->ppCuts[p->nCuts++], pCut );
+        if ( !fPreprocess )
-        p->nCutsMerged++;
+            If_CutCopy( p, pCutSet->ppCuts[pCutSet->nCuts++], pCut );
     }
 
-    // prepare room for the next cut
-    iCut = p->nCuts;
-    pCut = p->ppCuts[iCut];
     // generate cuts
     If_ObjForEachCut( pObj->pFanin0, pCut0, i )
     If_ObjForEachCut( pObj->pFanin1, pCut1, k )
     {
+        // get the next free cut
+        assert( pCutSet->nCuts <= pCutSet->nCutsMax );
+        pCut = pCutSet->ppCuts[pCutSet->nCuts];
         // make sure K-feasible cut exists
         if ( If_WordCountOnes(pCut0->uSign | pCut1->uSign) > p->pPars->nLutSize )
             continue;
         // merge the nodes
         if ( !If_CutMerge( pCut0, pCut1, pCut ) )
             continue;
+        assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+        p->nCutsMerged++;
         // check if this cut is contained in any of the available cuts
-        pCut->uSign = pCut0->uSign | pCut1->uSign;
 //        if ( p->pPars->pFuncCost == NULL && If_CutFilter( p, pCut ) ) // do not filter functionality cuts
-        if ( If_CutFilter( p, pCut ) )
+        if ( If_CutFilter( pCutSet, pCut ) )
             continue;
-        // the cuts have been successfully merged
         // compute the truth table
         pCut->fCompl = 0;
         if ( p->pPars->fTruth )
@@ -129,6 +121,8 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode )
         // compute the application-specific cost and depth
         pCut->fUser = (p->pPars->pFuncCost != NULL);
         pCut->Cost = p->pPars->pFuncCost? p->pPars->pFuncCost(pCut) : 0;
+        if ( pCut->Cost == IF_COST_MAX )
+            continue;
         // check if the cut satisfies the required times
         pCut->Delay = If_CutDelay( p, pCut );
 //        printf( "%.2f ", pCut->Delay );
@@ -137,30 +131,26 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode )
         // compute area of the cut (this area may depend on the application specific cost)
         pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, IF_INFINITY ) : If_CutFlow( p, pCut );
         pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
-        // make sure the cut is the last one (after filtering it may not be so)
+        // insert the cut into storage
-        assert( pCut == p->ppCuts[iCut] );
+        If_CutSort( p, pCutSet, pCut );
-        p->ppCuts[iCut] = p->ppCuts[p->nCuts];
-        p->ppCuts[p->nCuts] = pCut;
-        // count the cut
-        p->nCuts++;
-        p->nCutsMerged++;
-        // prepare room for the next cut
-        iCut = p->nCuts;
-        pCut = p->ppCuts[iCut];
     } 
-    assert( p->nCuts > 0 );
+    assert( pCutSet->nCuts > 0 );
-    // sort if we have more cuts
+
-    If_ManSortCuts( p, Mode );
+    // add the trivial cut to the set
-    // decide how many cuts to use
+    If_ManSetupCutTriv( p, pCutSet->ppCuts[pCutSet->nCuts++], pObj->Id );
-    pObj->nCuts = IF_MIN( p->nCuts + 1, p->nCutsUsed );
+    assert( pCutSet->nCuts <= pCutSet->nCutsMax+1 );
-//printf( "%d(%d) ", p->nCuts, pObj->nCuts );
+
-    // take the first
+    // update the best cut
-    If_ObjForEachCutStart( pObj, pCut, i, 1 )
+    if ( !fPreprocess || pCutSet->ppCuts[0]->Delay <= pObj->Required + p->fEpsilon )
-        If_CutCopy( pCut, p->ppCuts[i-1] );
+        If_CutCopy( p, If_ObjCutBest(pObj), pCutSet->ppCuts[0] );
     assert( p->pPars->fSeqMap || If_ObjCutBest(pObj)->nLeaves > 1 );
+
     // ref the selected cut
     if ( Mode && pObj->nRefs > 0 )
         If_CutRef( p, If_ObjCutBest(pObj), IF_INFINITY );
+
+    // free the cuts
+    If_ManDerefNodeCutSet( p, pObj );
 }
 
 /**Function*************************************************************
@@ -174,70 +164,73 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode )
   SeeAlso     []
 
 ***********************************************************************/
-void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode )
+void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPreprocess )
 {
+    If_Set_t * pCutSet;
     If_Obj_t * pTemp;
     If_Cut_t * pCutTemp, * pCut;
-    int i, iCut;
+    int i;
     assert( pObj->pEquiv != NULL );
+
     // prepare
     if ( Mode && pObj->nRefs > 0 )
         If_CutDeref( p, If_ObjCutBest(pObj), IF_INFINITY );
-    // prepare room for the next cut
+
-    p->nCuts = 0;
+    // remove elementary cuts
-    iCut = p->nCuts;
-    pCut = p->ppCuts[iCut];
-    // generate cuts
     for ( pTemp = pObj; pTemp; pTemp = pTemp->pEquiv )
+        pTemp->pCutSet->nCuts--;
+
+    // update the cutset of the node
+    pCutSet = pObj->pCutSet;
+
+    // generate cuts
+    for ( pTemp = pObj->pEquiv; pTemp; pTemp = pTemp->pEquiv )
     {
-        If_ObjForEachCutStart( pTemp, pCutTemp, i, 1 )
+        assert( pTemp->nRefs == 0 );
+        assert( p->pPars->fSeqMap || pTemp->pCutSet->nCuts > 0 );
+        // go through the cuts of this node
+        If_ObjForEachCut( pTemp, pCutTemp, i )
         {
-            assert( pTemp->nCuts > 1 );
+            assert( p->pPars->fSeqMap || pCutTemp->nLeaves > 1 );
-            assert( pTemp == pObj || pTemp->nRefs == 0 );
+            // get the next free cut
+            assert( pCutSet->nCuts <= pCutSet->nCutsMax );
+            pCut = pCutSet->ppCuts[pCutSet->nCuts];
             // copy the cut into storage
-            If_CutCopy( pCut, pCutTemp );
+            If_CutCopy( p, pCut, pCutTemp );
             // check if this cut is contained in any of the available cuts
-            if ( If_CutFilter( p, pCut ) )
+            if ( If_CutFilter( pCutSet, pCut ) )
                 continue;
-            // the cuts have been successfully merged
             // check if the cut satisfies the required times
             assert( pCut->Delay == If_CutDelay( p, pCut ) );
             if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
                 continue;
             // set the phase attribute
-            pCut->fCompl ^= (pObj->fPhase ^ pTemp->fPhase);
+            assert( pCut->fCompl == 0 );
+            pCut->fCompl ^= (pObj->fPhase ^ pTemp->fPhase); // why ^= ?
             // compute area of the cut (this area may depend on the application specific cost)
             pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, IF_INFINITY ) : If_CutFlow( p, pCut );
             pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
-            // make sure the cut is the last one (after filtering it may not be so)
+            // insert the cut into storage
-            assert( pCut == p->ppCuts[iCut] );
+            If_CutSort( p, pCutSet, pCut );
-            p->ppCuts[iCut] = p->ppCuts[p->nCuts];
-            p->ppCuts[p->nCuts] = pCut;
-            // count the cut
-            p->nCuts++;
-            // prepare room for the next cut
-            iCut = p->nCuts;
-            pCut = p->ppCuts[iCut];
-            // quit if we exceeded the number of cuts
-            if ( p->nCuts >= p->pPars->nCutsMax * p->pPars->nCutsMax )
-                break;
         }
-        // quit if we exceeded the number of cuts
-        if ( p->nCuts >= p->pPars->nCutsMax * p->pPars->nCutsMax )
-            break;
     }
-    assert( p->nCuts > 0 );
+    assert( pCutSet->nCuts > 0 );
-    // sort if we have more cuts
+
-    If_ManSortCuts( p, Mode );
+    // add the trivial cut to the set
-    // decide how many cuts to use
+    If_ManSetupCutTriv( p, pCutSet->ppCuts[pCutSet->nCuts++], pObj->Id );
-    pObj->nCuts = IF_MIN( p->nCuts + 1, p->nCutsUsed );
+    assert( pCutSet->nCuts <= pCutSet->nCutsMax+1 );
-    // take the first
+
-    If_ObjForEachCutStart( pObj, pCut, i, 1 )
+    // update the best cut
-        If_CutCopy( pCut, p->ppCuts[i-1] );
+    if ( !fPreprocess || pCutSet->ppCuts[0]->Delay <= pObj->Required + p->fEpsilon )
+        If_CutCopy( p, If_ObjCutBest(pObj), pCutSet->ppCuts[0] );
     assert( p->pPars->fSeqMap || If_ObjCutBest(pObj)->nLeaves > 1 );
+
     // ref the selected cut
     if ( Mode && pObj->nRefs > 0 )
         If_CutRef( p, If_ObjCutBest(pObj), IF_INFINITY );
+
+    // free the cuts
+    If_ManDerefChoiceCutSet( p, pObj );
 }
 
 /**Function*************************************************************
@@ -251,12 +244,19 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode )
   SeeAlso     []
 
 ***********************************************************************/
-int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fRequired, char * pLabel )
+int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPreprocess, char * pLabel )
 {
 //    ProgressBar * pProgress;
     If_Obj_t * pObj;
     int i, clk = clock();
     assert( Mode >= 0 && Mode <= 2 );
+    // set the sorting function
+    if ( Mode || p->pPars->fArea ) // area
+        p->SortMode = 1;
+    else if ( p->pPars->fFancy )
+        p->SortMode = 2;
+    else
+        p->SortMode = 0;
     // set the cut number
     p->nCutsUsed   = nCutsUsed;
     p->nCutsMerged = 0;
@@ -265,25 +265,25 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fRequi
     If_ManForEachNode( p, pObj, i )
     {
 //        Extra_ProgressBarUpdate( pProgress, i, pLabel );
-        If_ObjPerformMappingAnd( p, pObj, Mode );
+        If_ObjPerformMappingAnd( p, pObj, Mode, fPreprocess );
         if ( pObj->fRepr )
-            If_ObjPerformMappingChoice( p, pObj, Mode );
+            If_ObjPerformMappingChoice( p, pObj, Mode, fPreprocess );
     }
 //    Extra_ProgressBarStop( pProgress );
+    // make sure the visit counters are all zero
+    If_ManForEachNode( p, pObj, i )
+        assert( pObj->nVisits == 0 );
     // compute required times and stats
-    if ( fRequired )
+    If_ManComputeRequired( p );
-    {
-        If_ManComputeRequired( p, Mode==0 );
     if ( p->pPars->fVerbose )
     {
-            char Symb = (Mode == 0)? 'D' : ((Mode == 1)? 'F' : 'A');
+        char Symb = fPreprocess? 'P' : ((Mode == 0)? 'D' : ((Mode == 1)? 'F' : 'A'));
-            printf( "%c:  Del = %6.2f. Area = %8.2f. Nets = %6d. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
+        printf( "%c:  Del = %6.2f. Ar = %8.2f. Net = %6d. Cut = %8d. ", 
-                Symb, p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
+            Symb, p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged );
         PRT( "T", clock() - clk );
 //    printf( "Max number of cuts = %d. Average number of cuts = %5.2f.\n", 
 //        p->nCutsMax, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
     }
-    }
     return 1;
 }
 

src/map/if/ifPrepro.c

@@ -1,175 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [ifPrepro.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [FPGA mapping based on priority cuts.]
-
-  Synopsis    [Selects the starting mapping.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - November 21, 2006.]
-
-  Revision    [$Id: ifPrepro.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "if.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static void If_ManPerformMappingMoveBestCut( If_Man_t * p, int iPosNew, int iPosOld );
-static void If_ManPerformMappingAdjust( If_Man_t * p, int nCuts );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Merges the results of delay, relaxed delay and area-based mapping.]
-
-  Description [Delay target may be different from minimum delay!!!]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void If_ManPerformMappingPreprocess( If_Man_t * p )
-{
-    float delayArea, delayDelay, delayPure;
-    int clk = clock();
-    assert( p->pPars->nCutsMax >= 4 );
-
-    // perform min-area mapping and move the cut to the end
-    p->pPars->fArea = 1;
-    If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 0, "Start delay" );
-    p->pPars->fArea = 0;
-    delayArea = If_ManDelayMax( p, 0 );
-    if ( p->pPars->DelayTarget != -1 && delayArea < p->pPars->DelayTarget - p->fEpsilon )
-        delayArea = p->pPars->DelayTarget;
-    If_ManPerformMappingMoveBestCut( p, p->pPars->nCutsMax - 1, 1 );
-
-    // perfrom min-delay mapping and move the cut to the end
-    p->pPars->fFancy = 1;
-    If_ManPerformMappingRound( p, p->pPars->nCutsMax - 1, 0, 0, "Start delay-2" );
-    p->pPars->fFancy = 0;
-    delayDelay = If_ManDelayMax( p, 0 );
-    if ( p->pPars->DelayTarget != -1 && delayDelay < p->pPars->DelayTarget - p->fEpsilon )
-        delayDelay = p->pPars->DelayTarget;
-    If_ManPerformMappingMoveBestCut( p, p->pPars->nCutsMax - 2, 1 );
-
-    // perform min-delay mapping
-    If_ManPerformMappingRound( p, p->pPars->nCutsMax - 2, 0, 0, "Start flow" );
-    delayPure = If_ManDelayMax( p, 0 );
-    if ( p->pPars->DelayTarget != -1 && delayPure < p->pPars->DelayTarget - p->fEpsilon )
-        delayPure = p->pPars->DelayTarget;
-
-    // decide what to do
-    if ( delayPure < delayDelay - p->fEpsilon && delayPure < delayArea - p->fEpsilon )
-    {
-        // copy the remaining two cuts
-        if ( p->pPars->nCutsMax > 4 )
-        {
-            If_ManPerformMappingMoveBestCut( p, 2, p->pPars->nCutsMax - 2 );
-            If_ManPerformMappingMoveBestCut( p, 3, p->pPars->nCutsMax - 1 );
-        }
-        If_ManComputeRequired( p, 1 );
-        If_ManPerformMappingAdjust( p, 4 );
-    }
-    else if ( delayDelay < delayArea - p->fEpsilon )
-    {
-        If_ManPerformMappingMoveBestCut( p, 1, p->pPars->nCutsMax - 2 );
-        If_ManPerformMappingMoveBestCut( p, 2, p->pPars->nCutsMax - 1 );
-        If_ManComputeRequired( p, 1 );
-        If_ManPerformMappingAdjust( p, 3 );
-    }
-    else
-    {
-        If_ManPerformMappingMoveBestCut( p, 1, p->pPars->nCutsMax - 1 );
-        If_ManComputeRequired( p, 1 );
-        If_ManPerformMappingAdjust( p, 2 );
-    }
-    If_ManComputeRequired( p, 1 );
-    if ( p->pPars->fVerbose )
-    {
-        printf( "S:  Del = %6.2f. Area = %8.2f. Nets = %6d. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
-            p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
-        PRT( "T", clock() - clk );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Moves the best cut to the given position.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void If_ManPerformMappingMoveBestCut( If_Man_t * p, int iPosNew, int iPosOld )
-{
-    If_Obj_t * pObj;
-    int i;
-    assert( iPosOld != iPosNew );
-    assert( iPosOld > 0 && iPosOld < p->pPars->nCutsMax );
-    assert( iPosNew > 0 && iPosNew < p->pPars->nCutsMax );
-    If_ManForEachNode( p, pObj, i )
-        If_CutCopy( pObj->Cuts + iPosNew, pObj->Cuts + iPosOld );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adjusts mapping for the given cuts.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void If_ManPerformMappingAdjust( If_Man_t * p, int nCuts )
-{
-    If_Cut_t * pCut, * pCutBest;
-    If_Obj_t * pObj;
-    int i, c;
-    assert( nCuts >= 2 && nCuts <= 4 );
-    If_ManForEachNode( p, pObj, i )
-    {
-        pCutBest = NULL;
-        for ( c = 1; c < nCuts; c++ )
-        {
-            pCut = pObj->Cuts + c;
-            pCut->Delay = If_CutDelay( p, pCut );
-            pCut->Area  = If_CutFlow( p, pCut );
-            assert( pCutBest || pCut->Delay < pObj->Required + p->fEpsilon );
-            if ( pCutBest == NULL || 
-                (pCut->Delay < pObj->Required + p->fEpsilon && 
-                 pCut->Area < pCutBest->Area - p->fEpsilon) )
-                pCutBest = pCut;
-        }
-        assert( pCutBest != NULL );
-        // check if we need to move
-        if ( pCutBest != pObj->Cuts + 1 )
-            If_CutCopy( pObj->Cuts + 1, pCutBest );
-        // set the number of cuts
-        pObj->nCuts = 2;
-    }
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-

src/map/if/ifReduce.c

@@ -52,11 +52,11 @@ void If_ManImproveMapping( If_Man_t * p )
 
     clk = clock();
     If_ManImproveExpand( p, p->pPars->nLutSize );
-    If_ManComputeRequired( p, 0 );
+    If_ManComputeRequired( p );
     if ( p->pPars->fVerbose )
     {
-        printf( "E:  Del = %6.2f. Area = %8.2f. Nets = %6d. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
+        printf( "E:  Del = %6.2f. Ar = %8.2f. Net = %6d. Cut = %8d. ", 
-            p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
+            p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged );
         PRT( "T", clock() - clk );
     }
 
@@ -488,6 +488,7 @@ void If_ManImproveNodeFaninCompact( If_Man_t * p, If_Obj_t * pObj, int nLimit, V
 ***********************************************************************/
 void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit )
 {
+/*
     If_Cut_t * pCut, * pCut0, * pCut1, * pCutR;
     If_Obj_t * pFanin0, * pFanin1;
     float AreaBef, AreaAft;
@@ -537,13 +538,14 @@ void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit )
         AreaAft = If_CutAreaDerefed( p, pCutR, IF_INFINITY );
         // update the best cut
         if ( AreaAft < AreaBef - p->fEpsilon && pCutR->Delay < pObj->Required + p->fEpsilon )
-            If_CutCopy( pCut, pCutR );
+            If_CutCopy( p, pCut, pCutR );
     }
     // recompute the delay of the best cut
     pCut->Delay = If_CutDelay( p, pCut );
     // ref the cut if the node is refed
     if ( pObj->nRefs > 0 )
         If_CutRef( p, pCut, IF_INFINITY );
+*/
 }
 
 /**Function*************************************************************
@@ -562,14 +564,8 @@ void If_ManImproveReduce( If_Man_t * p, int nLimit )
     If_Obj_t * pObj;
     int i;
     If_ManForEachNode( p, pObj, i )
-    {
-        if ( 278 == i )
-        {
-            int s = 0;
-        }
         If_ManImproveNodeReduce( p, pObj, nLimit );
 }
-}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/map/if/ifSeq.c

@@ -24,19 +24,13 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int  If_ManBinarySearchPeriod( If_Man_t * p, int Mode );
-static int  If_ManBinarySearch_rec( If_Man_t * p, int Mode, int FiMin, int FiMax );
-static int  If_ManPerformMappingRoundSeq( If_Man_t * p, int Mode, int nIter, char * pLabel );
-static int  If_ManPrepareMappingSeq( If_Man_t * p );
-static int  If_ObjPerformMappingLatch( If_Man_t * p, If_Obj_t * pObj );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Performs sequential mapping.]
+  Synopsis    [Prepares for sequential mapping by linking the latches.]
 
   Description []
                
@@ -45,230 +39,19 @@ static int  If_ObjPerformMappingLatch( If_Man_t * p, If_Obj_t * pObj );
   SeeAlso     []
 
 ***********************************************************************/
-int If_ManPerformMappingSeq( If_Man_t * p )
+void If_ManPrepareMappingSeq( If_Man_t * p )
 {
-    int PeriodBest, Mode = 0;
+    If_Obj_t * pObjLi, * pObjLo;
+    int i;
 
-    // collect nodes in the sequential order
+    // link the latch outputs (CIs) directly to the drivers of latch inputs (COs)
-    If_ManPrepareMappingSeq( p );
+    for ( i = 0; i < p->pPars->nLatches; i++ )
-
-    // perform combinational mapping to get the upper bound on the clock period
-    If_ManPerformMappingRound( p, 2, 0, 0, NULL );
-    p->RequiredGlo = If_ManDelayMax( p, 0 );
-
-    // set parameters
-    p->nCutsUsed = p->pPars->nCutsMax;
-    p->nAttempts = 0;
-    p->nMaxIters = 50;
-    p->Period    = (int)p->RequiredGlo;
-
-    // make sure the clock period words
-    if ( !If_ManBinarySearchPeriod( p, Mode ) )
     {
-        printf( "If_ManPerformMappingSeq(): The upper bound on the clock period cannot be computed.\n" );
+        pObjLi = If_ManLi( p, i );
-        return 0;
+        pObjLo = If_ManLo( p, i );
+        pObjLo->pFanin0 = If_ObjFanin0( pObjLi );
+        pObjLo->fCompl0 = If_ObjFaninC0( pObjLi );
     }
-
-    // perform binary search
-    PeriodBest = If_ManBinarySearch_rec( p, Mode, 0, p->Period );
-
-    // recompute the best l-values
-    if ( p->Period != PeriodBest )
-    {
-        p->Period = PeriodBest;
-        if ( !If_ManBinarySearchPeriod( p, Mode ) )
-        {
-            printf( "If_ManPerformMappingSeq(): The final clock period cannot be confirmed.\n" );
-            return 0;
-        }
-    }
-/*
-    // fix the problem with non-converged delays
-    If_ManForEachNode( p, pObj, i )
-        if ( pObj->LValue < -ABC_INFINITY/2 )
-            pObj->LValue = (float)0.0;
-    // write the retiming lags
-    p->vLags = Vec_IntStart( If_ManObjNum(p) + 1 );
-    If_ManForEachNode( p, pObj, i )
-        Vec_IntWriteEntry( vLags, i, Abc_NodeComputeLag(pObj->LValue, p->Period) );
-*/
-/*
-    // print the statistic into a file
-    {
-        FILE * pTable;
-        pTable = fopen( "iscas/seqmap__stats.txt", "a+" );
-        fprintf( pTable, "%d ", p->Period );
-        fprintf( pTable, "\n" );
-        fclose( pTable );
-    }
-*/
-    // print the result
-    if ( p->pPars->fLiftLeaves )
-    {
-//        if ( p->pPars->fVerbose )   
-            printf( "The best clock period is %3d. (Currently, network is not modified, so mapping will fail.)\n", p->Period );
-        return 0;
-    }
-//    if ( p->pPars->fVerbose )   
-        printf( "The best clock period is %3d.\n", p->Period );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs binary search for the optimal clock period.]
-
-  Description [Assumes that FiMin is infeasible while FiMax is feasible.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int If_ManBinarySearch_rec( If_Man_t * p, int Mode, int FiMin, int FiMax )
-{
-    assert( FiMin < FiMax );
-    if ( FiMin + 1 == FiMax )
-        return FiMax;
-    // compute the median
-    p->Period = FiMin + (FiMax - FiMin)/2;
-    if ( If_ManBinarySearchPeriod( p, Mode ) )
-        return If_ManBinarySearch_rec( p, Mode, FiMin, p->Period ); // Median is feasible
-    else 
-        return If_ManBinarySearch_rec( p, Mode, p->Period, FiMax ); // Median is infeasible
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if retiming with this clock period is feasible.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int If_ManBinarySearchPeriod( If_Man_t * p, int Mode )
-{
-    If_Obj_t * pObj;
-    int i, c, fConverged;
-    int fResetRefs = 0;
-
-    p->nAttempts++;
-
-    // set l-values of all nodes to be minus infinity, except PIs and constants
-    If_ManForEachObj( p, pObj, i )
-    {
-        pObj->nCuts = 1;
-        If_ObjSetLValue( pObj, -IF_FLOAT_LARGE );
-        if ( fResetRefs )
-            pObj->nRefs = 0;
-    }
-    If_ObjSetLValue( If_ManConst1(p), (float)0.0 );
-    If_ManForEachPi( p, pObj, i )
-        If_ObjSetLValue( pObj, (float)0.0 );
-
-    // reset references to their original state
-    if ( fResetRefs )
-    {
-        If_ManForEachObj( p, pObj, i )
-        {
-            if ( If_ObjIsCo(pObj) )
-                continue;
-            if ( pObj->pFanin0 ) pObj->pFanin0->nRefs++;
-            if ( pObj->pFanin1 ) pObj->pFanin1->nRefs++;
-        }
-    }
-
-    // update all values iteratively
-    fConverged = 0;
-    for ( c = 1; c <= p->nMaxIters; c++ )
-    {
-        if ( !If_ManPerformMappingRoundSeq( p, Mode, c, NULL ) )
-        {
-            fConverged = 1;
-            break;
-        }
-        p->RequiredGlo = If_ManDelayMax( p, 1 );
-        if ( p->RequiredGlo > p->Period + p->fEpsilon )
-            break; 
-    }
-
-    // report the results
-    if ( p->pPars->fVerbose )
-    {
-        p->AreaGlo = p->pPars->fLiftLeaves? 0/*If_ManScanMappingSeq(p)*/ : If_ManScanMapping(p);
-        printf( "Attempt = %2d.  Iters = %3d.  Area = %10.2f.  Fi = %6.2f.  ", p->nAttempts, c, p->AreaGlo, (float)p->Period );
-        if ( fConverged )
-            printf( "  Feasible" );
-        else if ( c > p->nMaxIters )
-            printf( "Infeasible (timeout)" );
-        else
-            printf( "Infeasible" );
-        printf( "\n" );
-    }
-    return fConverged;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs one pass of l-value computation over all nodes.]
-
-  Description [Experimentally it was found that checking POs changes
-  is not enough to detect the convergence of l-values in the network.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int If_ManPerformMappingRoundSeq( If_Man_t * p, int Mode, int nIter, char * pLabel )
-{
-    ProgressBar * pProgress;
-    If_Obj_t * pObj;
-    int i, clk = clock();
-    int fVeryVerbose = 0;
-    int fChange = 0;
-    assert( Mode >= 0 && Mode <= 2 );
-    if ( !p->pPars->fVerbose )
-        pProgress = Extra_ProgressBarStart( stdout, If_ManObjNum(p) );
-    // map the internal nodes
-    p->nCutsMerged = 0;
-    If_ManForEachNode( p, pObj, i )
-    {
-        if ( !p->pPars->fVerbose )
-            Extra_ProgressBarUpdate( pProgress, i, pLabel );
-        // consider the camse of an AND gate
-        assert( If_ObjIsAnd(pObj) );
-        If_ObjPerformMappingAnd( p, pObj, Mode );
-        if ( pObj->fRepr )
-            If_ObjPerformMappingChoice( p, pObj, Mode );
-        // check if updating happens
-        if ( If_ObjLValue(pObj) < If_ObjCutBest(pObj)->Delay - p->fEpsilon )
-        {
-            If_ObjSetLValue( pObj, If_ObjCutBest(pObj)->Delay );
-            fChange = 1;
-        }
-//if ( If_ObjLValue(pObj) > -1000.0 )
-//printf( "Node %d %.2f  ", pObj->Id, If_ObjLValue(pObj) );
-    }
-    if ( !p->pPars->fVerbose )
-        Extra_ProgressBarStop( pProgress );
-    // propagate arrival times from the registers
-    Vec_PtrForEachEntry( p->vLatchOrder, pObj, i )
-        fChange |= If_ObjPerformMappingLatch( p, pObj );
-//printf( "\n\n" );
-    // compute area and delay
-    if ( fVeryVerbose )
-    {
-        p->RequiredGlo = If_ManDelayMax( p, 1 );
-        p->AreaGlo = p->pPars->fLiftLeaves? If_ManScanMappingSeq(p) : If_ManScanMapping(p);
-        printf( "S%d:  Fi = %6.2f. Del = %6.2f. Area = %8.2f. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
-             nIter, (float)p->Period, p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
-        PRT( "T", clock() - clk );
-    }
-    return fChange;
 }
 
 /**Function*************************************************************
@@ -311,7 +94,7 @@ Vec_Ptr_t * If_ManCollectLatches( If_Man_t * p )
     int i;
     // collect latches 
     vLatches = Vec_PtrAlloc( p->pPars->nLatches );
-    Vec_PtrForEachEntryStart( p->vCis, pObj, i, If_ManCiNum(p) - p->pPars->nLatches )
+    If_ManForEachLatchOutput( p, pObj, i )
         If_ManCollectLatches_rec( pObj, vLatches );
     // clean marks
     Vec_PtrForEachEntry( vLatches, pObj, i )
@@ -322,54 +105,71 @@ Vec_Ptr_t * If_ManCollectLatches( If_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Prepares for sequential mapping by linking the latches.]
+  Synopsis    [Performs one pass of l-value computation over all nodes.]
 
-  Description []
+  Description [Experimentally it was found that checking POs changes
+  is not enough to detect the convergence of l-values in the network.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int If_ManPrepareMappingSeq( If_Man_t * p )
+int If_ManPerformMappingRoundSeq( If_Man_t * p, int nIter )
 {
-    If_Obj_t * pObj, * pObjLi, * pObjLo, * pTemp;
+    If_Obj_t * pObj;
-    If_Cut_t * pCut;
+    int i, clk = clock();
-    int i;
+    int fVeryVerbose = 0;
-    // link the latch outputs (PIs) directly to the drivers of latch inputs (POs)
+    int fChange = 0;
-    for ( i = 0; i < p->pPars->nLatches; i++ )
+
+    // map the internal nodes
+    p->nCutsMerged = 0;
+    If_ManForEachNode( p, pObj, i )
     {
-        pObjLo = If_ManCi( p, If_ManCiNum(p) - p->pPars->nLatches + i );
+        If_ObjPerformMappingAnd( p, pObj, 0, 0 );
-        pObjLi = If_ManCo( p, If_ManCoNum(p) - p->pPars->nLatches + i );
+        if ( pObj->fRepr )
-        pObjLo->pFanin0 = If_ObjFanin0( pObjLi );
+            If_ObjPerformMappingChoice( p, pObj, 0, 0 );
-        pObjLo->fCompl0 = If_ObjFaninC0( pObjLi );
-//        pObjLo->pFanin0 = pObjLi;
     }
-    // collect latches
+
-    p->vLatchOrder = If_ManCollectLatches( p );
+    // postprocess the mapping
-    // propagate elementary cuts 
+//printf( "Itereation %d: \n", nIter );
-    if ( p->pPars->fLiftLeaves )
+    If_ManForEachNode( p, pObj, i )
     {
+        // update the LValues stored separately
+        if ( If_ObjLValue(pObj) < If_ObjCutBest(pObj)->Delay - p->fEpsilon )
+        {
+            If_ObjSetLValue( pObj, If_ObjCutBest(pObj)->Delay );
+            fChange = 1;
+        }
+//printf( "%d ", (int)If_ObjLValue(pObj) );
+        // reset the visit counters
+        assert( pObj->nVisits == 0 );
+        pObj->nVisits = pObj->nVisitsCopy;
+    }
+//printf( "\n" );
+
+    // propagate LValues over the registers
     Vec_PtrForEachEntry( p->vLatchOrder, pObj, i )
     {
-            pCut = If_ObjCutTriv(pObj);
+        If_ObjSetLValue( pObj, If_ObjLValue(If_ObjFanin0(pObj)) - p->Period );
-            If_CutCopy( pCut, If_ObjFanin0(pObj)->Cuts );
+        If_ObjSetArrTime( pObj, If_ObjLValue(pObj) );
-            If_CutLift( pCut );
+    }
-            pCut->Delay  -= p->Period;
-            pCut->fCompl ^= pObj->fCompl0;
 
-            // there is a bug here, which shows when there are choices...
+    // compute area and delay
-//            pTemp = If_ManObj(p, pCut->pLeaves[0] >> 8);
+    if ( fVeryVerbose )
-            pTemp = If_ManObj(p, pCut->pLeaves[0]);
+    {
-            assert( !If_ObjIsLatch(pTemp) );
+        p->RequiredGlo = If_ManDelayMax( p, 1 );
+        p->AreaGlo = If_ManScanMapping(p);
+        printf( "S%d:  Fi = %6.2f. Del = %6.2f. Area = %8.2f. Cuts = %8d. ", 
+             nIter, (float)p->Period, p->RequiredGlo, p->AreaGlo, p->nCutsMerged );
+        PRT( "T", clock() - clk );
     }
-    }
+    return fChange;
-    return 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Performs mapping of the latches.]
+  Synopsis    [Returns 1 if retiming with this clock period is feasible.]
 
   Description []
                
@@ -378,34 +178,204 @@ int If_ManPrepareMappingSeq( If_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int If_ObjPerformMappingLatch( If_Man_t * p, If_Obj_t * pObj )
+int If_ManBinarySearchPeriod( If_Man_t * p )
 {
-    If_Obj_t * pFanin;
+    If_Obj_t * pObj;
-    If_Cut_t * pCut;
+    int i, c, fConverged;
-    float LValueOld;
+    int fResetRefs = 0;
-    int i;
+
-    assert( If_ObjIsLatch(pObj) );
+    p->nAttempts++;
-    // save old l-value
+
-    LValueOld = If_ObjLValue(pObj);
+    // set LValues of of PIs to be 0 and other nodes to be -infinity
-    pFanin = If_ObjFanin0(pObj);
+    // LValues of the PIs are already set to 0
-    assert( pFanin->nCuts > 0 );
+    // undo any previous mapping, except for CIs
-    if ( !p->pPars->fLiftLeaves )
+    If_ManForEachObj( p, pObj, i )
     {
-        pObj->nCuts = 1;
+        if ( If_ObjIsPi(pObj) || If_ObjIsConst1(pObj) )
-        If_ObjSetLValue( pObj, If_ObjLValue(pFanin) - p->Period );
+            If_ObjSetLValue( pObj, (float)0.0 );
-    }
         else
+            If_ObjSetLValue( pObj, (float)-IF_INFINITY );
+        if ( If_ObjIsAnd(pObj) )
+            If_ObjCutBest(pObj)->nLeaves = 0;
+    }
+
+    // update all values iteratively
+    fConverged = 0;
+    for ( c = 1; c <= p->nMaxIters; c++ )
     {
-        pObj->nCuts = pFanin->nCuts;
+        if ( !If_ManPerformMappingRoundSeq( p, c ) )
-        If_ObjForEachCut( pObj, pCut, i )
         {
-            If_CutCopy( pCut, pFanin->Cuts + i );
+            p->RequiredGlo = If_ManDelayMax( p, 1 );
-            If_CutLift( pCut );
+            fConverged = 1;
-            pCut->Delay  -= p->Period;
+            break;
-            pCut->fCompl ^= pObj->fCompl0;
+        }
+        p->RequiredGlo = If_ManDelayMax( p, 1 );
+//printf( "Global = %d \n", (int)p->RequiredGlo );
+        if ( p->RequiredGlo > p->Period + p->fEpsilon )
+            break; 
+    }
+
+    // report the results
+    if ( p->pPars->fVerbose )
+    {
+        p->AreaGlo = If_ManScanMapping(p);
+        printf( "Attempt = %2d.  Iters = %3d.  Area = %10.2f.  Fi = %6.2f.  ", p->nAttempts, c, p->AreaGlo, (float)p->Period );
+        if ( fConverged )
+            printf( "  Feasible" );
+        else if ( c > p->nMaxIters )
+            printf( "Infeasible (timeout)" );
+        else
+            printf( "Infeasible" );
+        printf( "\n" );
+    }
+    return fConverged;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs binary search for the optimal clock period.]
+
+  Description [Assumes that FiMin is infeasible while FiMax is feasible.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManBinarySearch_rec( If_Man_t * p, int FiMin, int FiMax )
+{
+    assert( FiMin < FiMax );
+    if ( FiMin + 1 == FiMax )
+        return FiMax;
+    // compute the median
+    p->Period = FiMin + (FiMax - FiMin)/2;
+    if ( If_ManBinarySearchPeriod( p ) )
+        return If_ManBinarySearch_rec( p, FiMin, p->Period ); // Median is feasible
+    else 
+        return If_ManBinarySearch_rec( p, p->Period, FiMax ); // Median is infeasible
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs sequential mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManPerformMappingSeqPost( If_Man_t * p )
+{
+    If_Obj_t * pObjLi, * pObjLo, * pObj;
+    int i;
+
+    // link the latch outputs (CIs) directly to the drivers of latch inputs (COs)
+    for ( i = 0; i < p->pPars->nLatches; i++ )
+    {
+        pObjLi = If_ManLi( p, i );
+        pObjLo = If_ManLo( p, i );
+//        printf( "%3d : %2d -> %2d   \n", i, 
+//            (int)If_ObjLValue(If_ObjFanin0(pObjLo)), (int)If_ObjLValue(pObjLo) );
+    }
+
+    // set arrival times
+    assert( p->pPars->pTimesArr != NULL );
+    If_ManForEachLatchOutput( p, pObjLo, i )
+        p->pPars->pTimesArr[i] = If_ObjLValue(pObjLo);
+
+    // set the required times
+    assert( p->pPars->pTimesReq == NULL );
+    p->pPars->pTimesReq = ALLOC( float, If_ManCoNum(p) );
+    If_ManForEachPo( p, pObj, i )
+    {
+        p->pPars->pTimesReq[i] = p->RequiredGlo2;
+//        printf( "Out %3d : %2d   \n", i, (int)p->pPars->pTimesReq[i] );
+    }
+    If_ManForEachLatchInput( p, pObjLi, i )
+    {
+        p->pPars->pTimesReq[i] = If_ObjLValue(If_ObjFanin0(pObjLi));
+//        printf( "Out %3d : %2d   \n", i, (int)p->pPars->pTimesReq[i] );
+    }
+
+    // undo previous mapping
+    If_ManForEachObj( p, pObj, i )
+        if ( If_ObjIsAnd(pObj) )
+            If_ObjCutBest(pObj)->nLeaves = 0;
+
+    // map again combinationally
+    p->pPars->fSeqMap = 0;
+    If_ManPerformMappingComb( p );
+    p->pPars->fSeqMap = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs sequential mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManPerformMappingSeq( If_Man_t * p )
+{
+    int clkTotal = clock();
+    int PeriodBest;
+
+    p->SortMode = 0;
+
+    // perform combinational mapping to get the upper bound on the clock period
+    If_ManPerformMappingRound( p, 1, 0, 0, NULL );
+    p->RequiredGlo = If_ManDelayMax( p, 0 );
+    p->RequiredGlo2 = p->RequiredGlo;
+
+    // set direct linking of latches with their inputs
+    If_ManPrepareMappingSeq( p );
+
+    // collect latches
+    p->vLatchOrder = If_ManCollectLatches( p );
+
+    // set parameters
+    p->nCutsUsed = p->pPars->nCutsMax;
+    p->nAttempts = 0;
+    p->nMaxIters = 50;
+    p->Period    = (int)p->RequiredGlo;
+
+    // make sure the clock period works
+    if ( !If_ManBinarySearchPeriod( p ) )
+    {
+        printf( "If_ManPerformMappingSeq(): The upper bound on the clock period cannot be computed.\n" );
+        return 0;
+    }
+
+    // perform binary search
+    PeriodBest = If_ManBinarySearch_rec( p, 0, p->Period );
+
+    // recompute the best l-values
+    if ( p->Period != PeriodBest )
+    {
+        p->Period = PeriodBest;
+        if ( !If_ManBinarySearchPeriod( p ) )
+        {
+            printf( "If_ManPerformMappingSeq(): The final clock period cannot be confirmed.\n" );
+            return 0;
         }
     }
-    return LValueOld != If_ObjLValue(pObj);
+    if ( p->pPars->fVerbose )
+    {
+        printf( "The best clock period is %3d.  ", p->Period );
+        PRT( "Sequential time", clock() - clkTotal );
+    }
+    p->RequiredGlo = (float)PeriodBest;
+
+    // postprocess it using combinational mapping
+    If_ManPerformMappingSeqPost( p );
+    return 1;
 }
 
 ////////////////////////////////////////////////////////////////////////

src/map/if/ifUtil.c

@@ -61,11 +61,9 @@ void If_ManCleanNodeCopy( If_Man_t * p )
 void If_ManCleanCutData( If_Man_t * p )
 {
     If_Obj_t * pObj;
-    If_Cut_t * pCut;
+    int i;
-    int i, k;
     If_ManForEachObj( p, pObj, i )
-        If_ObjForEachCut( pObj, pCut, k )
+        If_CutSetData( If_ObjCutBest(pObj), NULL );
-            If_CutSetData( pCut, NULL );
 }
 
 /**Function*************************************************************
@@ -113,20 +111,20 @@ float If_ManDelayMax( If_Man_t * p, int fSeq )
     {
         assert( p->pPars->nLatches > 0 );
         If_ManForEachPo( p, pObj, i )
-            if ( DelayBest < If_ObjCutBest( If_ObjFanin0(pObj) )->Delay )
+            if ( DelayBest < If_ObjArrTime(If_ObjFanin0(pObj)) )
-                 DelayBest = If_ObjCutBest( If_ObjFanin0(pObj) )->Delay;
+                 DelayBest = If_ObjArrTime(If_ObjFanin0(pObj));
     }
     else if ( p->pPars->fLatchPaths )
     {
-        If_ManForEachLatch( p, pObj, i )
+        If_ManForEachLatchInput( p, pObj, i )
-            if ( DelayBest < If_ObjCutBest( If_ObjFanin0(pObj) )->Delay )
+            if ( DelayBest < If_ObjArrTime(If_ObjFanin0(pObj)) )
-                 DelayBest = If_ObjCutBest( If_ObjFanin0(pObj) )->Delay;
+                 DelayBest = If_ObjArrTime(If_ObjFanin0(pObj));
     }
     else 
     {
         If_ManForEachCo( p, pObj, i )
-            if ( DelayBest < If_ObjCutBest( If_ObjFanin0(pObj) )->Delay )
+            if ( DelayBest < If_ObjArrTime(If_ObjFanin0(pObj)) )
-                 DelayBest = If_ObjCutBest( If_ObjFanin0(pObj) )->Delay;
+                 DelayBest = If_ObjArrTime(If_ObjFanin0(pObj));
     }
     return DelayBest;
 }
@@ -142,13 +140,30 @@ float If_ManDelayMax( If_Man_t * p, int fSeq )
   SeeAlso     []
 
 ***********************************************************************/
-void If_ManComputeRequired( If_Man_t * p, int fFirstTime )
+void If_ManComputeRequired( If_Man_t * p )
 {
     If_Obj_t * pObj;
     int i;
+
     // compute area, clean required times, collect nodes used in the mapping
     p->nNets = 0;
     p->AreaGlo = If_ManScanMapping( p );
+
+    // consider the case when the required times are given
+    if ( p->pPars->pTimesReq )
+    {
+        assert( !p->pPars->fAreaOnly );
+        // make sure that the required time hold
+        If_ManForEachCo( p, pObj, i )
+        {
+            if ( If_ObjArrTime(If_ObjFanin0(pObj)) > p->pPars->pTimesReq[i] + p->fEpsilon )
+                printf( "Required times are violated for output %d (arr = %d; req = %d).\n", 
+                    i, (int)If_ObjArrTime(If_ObjFanin0(pObj)), (int)p->pPars->pTimesReq[i] );
+            If_ObjFanin0(pObj)->Required = p->pPars->pTimesReq[i];
+        }
+    }
+    else
+    {
         // get the global required times
         p->RequiredGlo = If_ManDelayMax( p, 0 );
         // update the required times according to the target
@@ -156,20 +171,29 @@ void If_ManComputeRequired( If_Man_t * p, int fFirstTime )
         {
             if ( p->RequiredGlo > p->pPars->DelayTarget + p->fEpsilon )
             {
-            if ( fFirstTime )
+                if ( p->fNextRound == 0 )
+                {
+                    p->fNextRound = 1;
                     printf( "Cannot meet the target required times (%4.2f). Mapping continues anyway.\n", p->pPars->DelayTarget );
                 }
+            }
             else if ( p->RequiredGlo < p->pPars->DelayTarget - p->fEpsilon )
             {
-            if ( fFirstTime )
+                if ( p->fNextRound == 0 )
+                {
+                    p->fNextRound = 1;
                     printf( "Relaxing the required times from (%4.2f) to the target (%4.2f).\n", p->RequiredGlo, p->pPars->DelayTarget );
+                }
                 p->RequiredGlo = p->pPars->DelayTarget;
             }
         }
+        // do not propagate required times if area minimization is requested
+        if ( p->pPars->fAreaOnly ) 
+            return;
         // set the required times for the POs
         if ( p->pPars->fLatchPaths )
         {
-        If_ManForEachLatch( p, pObj, i )
+            If_ManForEachLatchInput( p, pObj, i )
                 If_ObjFanin0(pObj)->Required = p->RequiredGlo;
         }
         else 
@@ -177,6 +201,7 @@ void If_ManComputeRequired( If_Man_t * p, int fFirstTime )
             If_ManForEachCo( p, pObj, i )
                 If_ObjFanin0(pObj)->Required = p->RequiredGlo;
         }
+    }
     // go through the nodes in the reverse topological order
     Vec_PtrForEachEntry( p->vMapped, pObj, i )
         If_CutPropagateRequired( p, If_ObjCutBest(pObj), pObj->Required );
@@ -236,6 +261,7 @@ float If_ManScanMapping( If_Man_t * p )
     If_ManForEachObj( p, pObj, i )
     {
         pObj->Required = IF_FLOAT_LARGE;
+        pObj->nVisits  = pObj->nVisitsCopy;
         pObj->nRefs    = 0;
     }
     // allocate place to store the nodes
@@ -318,6 +344,83 @@ float If_ManScanMappingSeq( If_Man_t * p )
     return aArea;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes area, references, and nodes used in the mapping.]
+
+  Description [Collects the nodes in reverse topological order in array 
+  p->vMapping.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManResetOriginalRefs( If_Man_t * p )
+{
+    If_Obj_t * pObj;
+    int i;
+    If_ManForEachObj( p, pObj, i )
+        pObj->nRefs = 0;
+    If_ManForEachObj( p, pObj, i )
+    {
+        if ( If_ObjIsAnd(pObj) )
+        {
+            pObj->pFanin0->nRefs++;
+            pObj->pFanin1->nRefs++;
+        }
+        else if ( If_ObjIsCo(pObj) )
+            pObj->pFanin0->nRefs++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes cross-cut of the circuit.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManCrossCut( If_Man_t * p )
+{
+    If_Obj_t * pObj, * pFanin;
+    int i, nCutSize = 0, nCutSizeMax = 0;
+    If_ManForEachObj( p, pObj, i )
+    {
+        if ( !If_ObjIsAnd(pObj) )
+            continue;
+        // consider the node
+        if ( nCutSizeMax < ++nCutSize )
+            nCutSizeMax = nCutSize;
+        if ( pObj->nVisits == 0 )
+            nCutSize--;
+        // consider the fanins
+        pFanin = If_ObjFanin0(pObj);
+        if ( !If_ObjIsCi(pFanin) && --pFanin->nVisits == 0 )
+            nCutSize--;
+        pFanin = If_ObjFanin1(pObj);
+        if ( !If_ObjIsCi(pFanin) && --pFanin->nVisits == 0 )
+            nCutSize--;
+        // consider the choice class
+        if ( pObj->fRepr )
+            for ( pFanin = pObj; pFanin; pFanin = pFanin->pEquiv )
+                if ( !If_ObjIsCi(pFanin) && --pFanin->nVisits == 0 )
+                    nCutSize--;
+    }
+    If_ManForEachObj( p, pObj, i )
+    {
+        assert( If_ObjIsCi(pObj) || pObj->fVisit == 0 );
+        pObj->nVisits = pObj->nVisitsCopy;
+    }
+    assert( nCutSize == 0 );
+//    printf( "Max cross cut size = %6d.\n", nCutSizeMax );
+    return nCutSizeMax;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/map/if/module.make

@@ -2,7 +2,6 @@ SRC +=  src/map/if/ifCore.c \
     src/map/if/ifCut.c \
     src/map/if/ifMan.c \
     src/map/if/ifMap.c \
-    src/map/if/ifPrepro.c \
     src/map/if/ifReduce.c \
     src/map/if/ifSeq.c \
     src/map/if/ifTime.c \

src/map/mio/mioRead.c

@@ -49,7 +49,7 @@ extern int          isspace( int c );  // to silence the warning in VS
   SeeAlso     []
 
 ***********************************************************************/
-Mio_Library_t * Mio_LibraryRead( Abc_Frame_t * pAbc, char * FileName, char * ExcludeFile, int fVerbose )
+Mio_Library_t * Mio_LibraryRead( void * pAbc, char * FileName, char * ExcludeFile, int fVerbose )
 {
     Mio_Library_t * pLib;
     int num;
@@ -486,7 +486,7 @@ void Mio_LibraryDetectSpecialGates( Mio_Library_t * pLib )
   SeeAlso     []
 
 ***********************************************************************/
-int Mio_LibraryReadExclude( Abc_Frame_t * pAbc, char * ExcludeFile, st_table * tExcludeGate )
+int Mio_LibraryReadExclude( void * pAbc, char * ExcludeFile, st_table * tExcludeGate )
 {
     int nDel = 0;
     FILE *pEx;

src/misc/extra/extra.h

@@ -349,6 +349,7 @@ extern char *      Extra_MmFixedEntryFetch( Extra_MmFixed_t * p );
 extern void        Extra_MmFixedEntryRecycle( Extra_MmFixed_t * p, char * pEntry );
 extern void        Extra_MmFixedRestart( Extra_MmFixed_t * p );
 extern int         Extra_MmFixedReadMemUsage( Extra_MmFixed_t * p );
+extern int         Extra_MmFixedReadMaxEntriesUsed( Extra_MmFixed_t * p );
 // flexible-size-block memory manager
 extern Extra_MmFlex_t * Extra_MmFlexStart();
 extern void        Extra_MmFlexStop( Extra_MmFlex_t * p );

src/misc/extra/extraUtilMemory.c

@@ -310,6 +310,21 @@ int Extra_MmFixedReadMemUsage( Extra_MmFixed_t * p )
     return p->nMemoryAlloc;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_MmFixedReadMaxEntriesUsed( Extra_MmFixed_t * p )
+{
+    return p->nEntriesMax;
+}
 
 
 /**Function*************************************************************
@@ -326,7 +341,7 @@ int Extra_MmFixedReadMemUsage( Extra_MmFixed_t * p )
 Extra_MmFlex_t * Extra_MmFlexStart()
 {
     Extra_MmFlex_t * p;
-
+//printf( "allocing flex\n" );
     p = ALLOC( Extra_MmFlex_t, 1 );
     memset( p, 0, sizeof(Extra_MmFlex_t) );
 
@@ -379,6 +394,7 @@ void Extra_MmFlexStop( Extra_MmFlex_t * p )
     int i;
     if ( p == NULL )
         return;
+//printf( "deleting flex\n" );
     for ( i = 0; i < p->nChunks; i++ )
         free( p->pChunks[i] );
     free( p->pChunks );

src/misc/vec/vecStr.h

@@ -401,6 +401,59 @@ static inline void Vec_StrPush( Vec_Str_t * p, char Entry )
     p->pArray[p->nSize++] = Entry;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrPrintNum( Vec_Str_t * p, int Num )
+{
+    int i, nDigits;
+    if ( Num < 0 )
+    {
+        Vec_StrPush( p, '-' );
+        Num = -Num;
+    }
+    if ( Num < 10 )
+    {
+        Vec_StrPush( p, (char)('0' + Num) );
+        return;
+    }
+    nDigits = Extra_Base10Log( Num );
+    Vec_StrGrow( p, p->nSize + nDigits );
+    for ( i = nDigits - 1; i >= 0; i-- )
+    {
+        Vec_StrWriteEntry( p, p->nSize + i, (char)('0' + Num % 10) );
+        Num /= 10;
+    }
+    assert( Num == 0 );
+    p->nSize += nDigits;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrPrintStr( Vec_Str_t * p, char * pStr )
+{
+    int i, Length = strlen(pStr);
+    for ( i = 0; i < Length; i++ )
+        Vec_StrPush( p, pStr[i] );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Appends the string to the char vector.]

src/phys/place/libhmetis.h

@@ -3,7 +3,7 @@
 #ifndef LIBHMETIS_H_
 #define LIBHMETIS_H_
 
-void HMETIS_PartRecursive(int nvtxs, 
+static void HMETIS_PartRecursive(int nvtxs, 
               int nhedges, 
               int *vwgts, 
               int *eptr,
@@ -13,10 +13,10 @@ void HMETIS_PartRecursive(int nvtxs,
               int nbfactor, 
               int *options, 
               int *part, 
-              int *edgecnt );
+              int *edgecnt ) {} //;
 
 
-void HMETIS_PartKway(int nvtxs, 
+static void HMETIS_PartKway(int nvtxs, 
              int nhedges, 
              int *vwgts, 
              int *eptr, 
@@ -26,6 +26,6 @@ void HMETIS_PartKway(int nvtxs,
              int nbfactor, 
              int *options, 
              int *part, 
-             int *edgecnt );
+             int *edgecnt ) {} //;
 
 #endif