Improving MFFC computation code.

8 files changed, 202 insertions, 173 deletions

diff --git a/src/aig/gia/giaSim4.c b/src/aig/gia/giaSim4.c
index 6ce89cf0..56dcb713 100644
--- a/src/aig/gia/giaSim4.c
+++ b/src/aig/gia/giaSim4.c
@@ -41,7 +41,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fVerbose )
+int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fSkipMffc, int fVerbose )
 {
     return 0;
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7b4db87a..76f60a36 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -7194,11 +7194,11 @@ usage:
 ***********************************************************************/
 int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fRandom, int fUseWeights, int fInputs, int fVerbose, int fVeryVerbose );
+    extern void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fRandom, int fUseWeights, int fInputs, int fSkipMffc, int fVerbose, int fVeryVerbose );
     char * pFileNames[4] = {NULL, NULL, "out.v", NULL};
-    int c, nWords = 8, nBeam = 4, LevL = -1, LevU = -1, fOrder = 0, fFancy = 0, fUseBuf = 0, fRandom = 0, fUseWeights = 0, fInputs = 0, fVerbose = 0, fVeryVerbose = 0;
+    int c, nWords = 8, nBeam = 4, LevL = -1, LevU = -1, fOrder = 0, fFancy = 0, fUseBuf = 0, fRandom = 0, fUseWeights = 0, fInputs = 0, fSkipMffc = 0, fVerbose = 0, fVeryVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WBLUofbruivwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WBLUofbruimvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7264,6 +7264,9 @@ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'i':
             fInputs ^= 1;
             break;
+        case 'm':
+            fSkipMffc ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -7295,11 +7298,11 @@ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv )
         else
             fclose( pFile );
     }
-    Acb_NtkRunSim( pFileNames, nWords, nBeam, LevL, LevU, fOrder, fFancy, fUseBuf, fRandom, fUseWeights, fInputs, fVerbose, fVeryVerbose );
+    Acb_NtkRunSim( pFileNames, nWords, nBeam, LevL, LevU, fOrder, fFancy, fUseBuf, fRandom, fUseWeights, fInputs, fSkipMffc, fVerbose, fVeryVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: runsim [-WBLU] [-ofbruivwh] [-N <num>] <file1> <file2> <file3>\n" );
+    Abc_Print( -2, "usage: runsim [-WBLU] [-ofbruimvwh] [-N <num>] <file1> <file2> <file3>\n" );
     Abc_Print( -2, "\t           experimental simulation command\n" );
     Abc_Print( -2, "\t-W <num> : the number of words of simulation info [default = %d]\n", nWords );
     Abc_Print( -2, "\t-B <num> : the beam width parameter [default = %d]\n", nBeam );
@@ -7311,6 +7314,7 @@ usage:
     Abc_Print( -2, "\t-r       : toggle using random permutation of support variables [default = %s]\n",      fRandom? "yes": "no" );
     Abc_Print( -2, "\t-u       : toggle using topological info to select support variables [default = %s]\n", fUseWeights? "yes": "no" );
     Abc_Print( -2, "\t-i       : toggle using primary inputs as support variables [default = %s]\n",          fInputs? "yes": "no" );
+    Abc_Print( -2, "\t-m       : toggle MFFC nodes as candidate divisors [default = %s]\n",                   fSkipMffc? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggle printing verbose information [default = %s]\n",                       fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w       : toggle printing more verbose information [default = %s]\n",                  fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");
diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c
index 6d5bdaad..cc9c425b 100644
--- a/src/base/acb/acbFunc.c
+++ b/src/base/acb/acbFunc.c
@@ -1942,44 +1942,17 @@ Vec_Int_t * Acb_GetUsedDivs( Vec_Int_t * vDivs, Vec_Int_t * vUsed )
         Vec_IntPush( vRes, iObj );
     return vRes;
 }
-Vec_Int_t * Acb_GetDerefedNodes( Acb_Ntk_t * p )
-{
-    Vec_Ptr_t * vNames = Abc_FrameReadSignalNames();
-    if ( vNames != NULL )
-    {
-        Vec_Int_t * vNodes = Vec_IntAlloc( 100 );
-        Vec_Int_t * vMap   = Vec_IntStartFull( Abc_NamObjNumMax(p->pDesign->pStrs) );
-        int i, iObj; char * pName;
-        Acb_NtkForEachObj( p, iObj )
-            if ( Acb_ObjName(p, iObj) )
-                Vec_IntWriteEntry( vMap, Acb_ObjName(p, iObj), iObj );
-        Vec_PtrForEachEntry( char *, vNames, pName, i )
-        {
-            int NameId = Abc_NamStrFindOrAdd( p->pDesign->pStrs, pName, NULL );
-            if ( NameId == 0 )
-            {
-                printf( "Cannot find name ID for name %s\n", pName );
-                Vec_IntFree( vMap );
-                Vec_IntFree( vNodes );
-                return NULL;
-            }
-            else if ( Vec_IntEntry(vMap, NameId) == -1 )
-            {
-                printf( "Cannot find obj ID for name %s\n", pName );
-                Vec_IntFree( vMap );
-                Vec_IntFree( vNodes );
-                return NULL;
-            }
-            else
-                Vec_IntPush( vNodes, Vec_IntEntry(vMap, NameId) );
-        }
-        Vec_IntFree( vMap );
-        return vNodes;
-    }
-    return NULL;
+Vec_Ptr_t * Acb_SignalNames( Acb_Ntk_t * p, Vec_Int_t * vObjs )
+{
+    Vec_Ptr_t * vNames = Vec_PtrAlloc( Vec_IntSize(vObjs) );
+    int i, iObj;
+    Vec_IntForEachEntry( vObjs, iObj, i )
+        Vec_PtrPush( vNames, Acb_ObjNameStr(p, iObj) );
+    return vNames;
 }
 Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUsed, Vec_Ptr_t * vSops, Vec_Ptr_t * vGias, Vec_Int_t * vTars )
 {
+    extern int Acb_NtkCollectMfsGates( char * pFileName, Vec_Ptr_t * vNamesRefed, Vec_Ptr_t * vNamesDerefed, int nGates1[5] );
     extern Vec_Wec_t * Abc_SopSynthesize( Vec_Ptr_t * vSops );
     extern Vec_Wec_t * Abc_GiaSynthesize( Vec_Ptr_t * vGias, Gia_Man_t * pMulti );
     Vec_Wec_t * vGates = vGias ? Abc_GiaSynthesize(vGias, NULL) : Abc_SopSynthesize(vSops);  Vec_Int_t * vGate;
@@ -1989,15 +1962,13 @@ Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUs
     Vec_Ptr_t * vNames = Acb_GenerateSignalNames( p, vDivs, vUsed, nWires, vTars, vGates );
     Vec_Str_t * vStr = Vec_StrAlloc( 100 );
     Vec_Int_t * vSup = Acb_GetUsedDivs( vDivs, vUsed );
-    Vec_Int_t * vDrf = Acb_GetDerefedNodes( p );
+    Vec_Ptr_t * vSpN = Acb_SignalNames( p, vSup );
     Vec_Int_t * vTfi = Acb_ObjCollectTfiVec( p, vSup );
     Vec_Int_t * vTfo = Acb_ObjCollectTfoVec( p, vTars );
     int nPiCount = Acb_NtkCountPiBuffers( p, vSup );
     int nPoCount = Acb_NtkCountPoDrivers( p, vTars );
-    int nMffc    = vDrf ? Vec_IntSize(vTars) + Acb_NtkFindMffcSize( p, vSup, vDrf, nGates1 ) : 0;
-    int * pCounts = Abc_FrameReadGateCounts();
-    for ( i = 0; i < 5; i++ )
-        nGates1[i] += pCounts[i];
+    int nMffc    = Abc_FrameReadSpecName() ? Acb_NtkCollectMfsGates( Abc_FrameReadSpecName(), vSpN, Abc_FrameReadSignalNames(), nGates1 ) : 0;
+    Vec_PtrFree( vSpN );
     Vec_IntFree( vSup );
     Vec_WecForEachLevelStartStop( vGates, vGate, i, Vec_IntSize(vUsed), Vec_IntSize(vUsed)+nWires )
     {
@@ -2017,9 +1988,9 @@ Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUs
 
     Vec_StrPrintF( vStr, "// Patch   : in = %d  out = %d : pi_in = %d  po_out = %d : tfi = %d  tfo = %d\n", Vec_IntSize(vUsed), nOuts, nPiCount, nPoCount, Vec_IntSize(vTfi), Vec_IntSize(vTfo) );
     Vec_StrPrintF( vStr, "// Added   : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n", nWires,         nGates0[0], nGates0[1], nGates0[2], nGates0[3], nGates0[4] ); 
-    if ( vDrf != NULL )
+    if ( Abc_FrameReadSpecName() )
     Vec_StrPrintF( vStr, "// Removed : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n", nMffc,          nGates1[0], nGates1[1], nGates1[2], nGates1[3], nGates1[4] ); 
-    if ( vDrf != NULL )
+    if ( Abc_FrameReadSpecName() )
     Vec_StrPrintF( vStr, "// TOTAL   : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n", nWires-nMffc, nGates0[0]-nGates1[0],  nGates0[1]-nGates1[1],  nGates0[2]-nGates1[2], nGates0[3]-nGates1[3], nGates0[4]-nGates1[4] ); 
     Vec_StrPrintF( vStr, "\n" );
 
@@ -2084,12 +2055,11 @@ Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUs
     printf( "\n" );
     printf( "Patch   : in = %d  out = %d : pi_in = %d  po_out = %d : tfi = %d  tfo = %d\n", Vec_IntSize(vUsed), nOuts, nPiCount, nPoCount, Vec_IntSize(vTfi), Vec_IntSize(vTfo) );
     printf( "Added   : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n", nWires,         nGates0[0], nGates0[1], nGates0[2], nGates0[3], nGates0[4] ); 
-    if ( vDrf != NULL )
+    if ( Abc_FrameReadSpecName() )
     printf( "Removed : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n", nMffc,          nGates1[0], nGates1[1], nGates1[2], nGates1[3], nGates1[4] ); 
-    if ( vDrf != NULL )
+    if ( Abc_FrameReadSpecName() )
     printf( "TOTAL   : gate =%4d : c0 =%2d  c1 =%2d  buf =%3d  inv =%3d  two-input =%4d\n", nWires-nMffc,   nGates0[0]-nGates1[0],  nGates0[1]-nGates1[1],  nGates0[2]-nGates1[2], nGates0[3]-nGates1[3], nGates0[4]-nGates1[4] ); 
     printf( "\n" );
-    Vec_IntFreeP( &vDrf );
     return vStr;
 }
 
@@ -2209,11 +2179,11 @@ Vec_Str_t * Acb_GeneratePatch2( Gia_Man_t * pGia, Vec_Ptr_t * vIns, Vec_Ptr_t *
     printf( "Synthesized patch with %d inputs, %d outputs and %d gates.\n", nIns, nOuts, nWires );
     return vStr;
 }
-void Acb_GenerateFile2( Gia_Man_t * pGia, Vec_Ptr_t * vIns, Vec_Ptr_t * vOuts, char * pFileName, char * pFileNameOut )
+void Acb_GenerateFile2( Gia_Man_t * pGia, Vec_Ptr_t * vIns, Vec_Ptr_t * vOuts, char * pFileName, char * pFileNameOut, int fSkipMffc )
 {
     extern void Acb_GenerateFilePatch( Vec_Str_t * p, char * pFileNamePatch );
     extern void Acb_GenerateFileOut( Vec_Str_t * vPatchLine, char * pFileNameF, char * pFileNameOut, Vec_Str_t * vPatch );
-    extern void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames, int fNumber );
+    extern void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames, int fNumber, int fSkipMffc );
     Vec_Str_t * vInst   = Acb_GenerateInstance2( vIns, vOuts );
     Vec_Str_t * vPatch  = Acb_GeneratePatch2( pGia, vIns, vOuts );
     //printf( "%s", Vec_StrArray(vPatch) );
@@ -2221,7 +2191,7 @@ void Acb_GenerateFile2( Gia_Man_t * pGia, Vec_Ptr_t * vIns, Vec_Ptr_t * vOuts, c
     // generate output files
     Acb_GenerateFilePatch( vPatch, "patch.v" );
     printf( "Finished dumping patch file \"%s\".\n", "patch.v" );
-    Acb_NtkInsert( pFileName, "temp.v", vOuts, 0 );
+    Acb_NtkInsert( pFileName, "temp.v", vOuts, 0, fSkipMffc );
     printf( "Finished dumping intermediate file \"%s\".\n", "temp.v" );
     Acb_GenerateFileOut( vInst, "temp.v", pFileNameOut, vPatch );
     printf( "Finished dumping the resulting file \"%s\".\n", pFileNameOut );
diff --git a/src/base/acb/acbUtil.c b/src/base/acb/acbUtil.c
index 070754af..2cfae6ea 100644
--- a/src/base/acb/acbUtil.c
+++ b/src/base/acb/acbUtil.c
@@ -148,9 +148,13 @@ int Acb_NtkCountPoDrivers( Acb_Ntk_t * p, Vec_Int_t * vObjs )
     int i, iObj, Count = 0;
     Acb_NtkIncTravId( p );
     Acb_NtkForEachCo( p, iObj, i )
+    {
+        int Fanin0 = Acb_ObjFanin0(p, iObj);
         Acb_ObjSetTravIdCur( p, iObj );
-    Acb_NtkForEachCo( p, iObj, i )
-        Acb_ObjSetTravIdCur( p, Acb_ObjFanin(p, iObj, 0) );
+        Acb_ObjSetTravIdCur( p, Fanin0 );
+        if ( Acb_ObjFaninNum(p, Fanin0) == 1 )
+            Acb_ObjSetTravIdCur( p, Acb_ObjFanin0(p, Fanin0) );
+    }
     Vec_IntForEachEntry( vObjs, iObj, i )
         Count += Acb_ObjIsTravIdCur(p, iObj);
     return Count;
@@ -167,47 +171,117 @@ int Acb_NtkCountPoDrivers( Acb_Ntk_t * p, Vec_Int_t * vObjs )
   SeeAlso     []
 
 ***********************************************************************/
-int Acb_NtkNodeDeref_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj, int nGates[5] )
+int Acb_NtkNodeDeref_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj )
 {
     int i, Fanin, * pFanins, Counter = 1;
     if ( Acb_ObjIsCi(p, iObj) )
         return 0;
-    if ( nGates )
-    {
-        int nFan = Acb_ObjFaninNum(p, iObj);
-        int Type = Acb_ObjType( p, iObj );
-        if ( Type == ABC_OPER_CONST_F ) 
-            nGates[0]++;
-        else if ( Type == ABC_OPER_CONST_T ) 
-            nGates[1]++;
-        else if ( Type == ABC_OPER_BIT_BUF || Type == ABC_OPER_CO ) 
-            nGates[2]++;
-        else if ( Type == ABC_OPER_BIT_INV ) 
-            nGates[3]++;
-        else
-        {
-            assert( nFan >= 2 );
-            nGates[4] += Acb_ObjFaninNum(p, iObj)-1;
-        }
-    }
     Acb_ObjForEachFaninFast( p, iObj, pFanins, Fanin, i )
     {
         assert( Vec_IntEntry(vRefs, Fanin) > 0 );
         Vec_IntAddToEntry( vRefs, Fanin, -1 );
         if ( Vec_IntEntry(vRefs, Fanin) == 0 )
-            Counter += Acb_NtkNodeDeref_rec( vRefs, p, Fanin, nGates );
+            Counter += Acb_NtkNodeDeref_rec( vRefs, p, Fanin );
     }
     return Counter;
 }
-int Acb_NtkNodeRef_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj, int nGates[5] )
+int Acb_NtkNodeRef_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj )
 {
     int i, Fanin, * pFanins, Counter = 1;
     if ( Acb_ObjIsCi(p, iObj) )
         return 0;
-    if ( nGates )
+    Acb_ObjForEachFaninFast( p, iObj, pFanins, Fanin, i )
     {
-        int nFan = Acb_ObjFaninNum(p, iObj);
-        int Type = Acb_ObjType( p, iObj );
+        if ( Vec_IntEntry(vRefs, Fanin) == 0 )
+            Counter += Acb_NtkNodeRef_rec( vRefs, p, Fanin );
+        Vec_IntAddToEntry( vRefs, Fanin, 1 );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computing and updating direct and reverse logic level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acb_NtkCollectDeref_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj, Vec_Int_t * vRes )
+{
+    int i, Fanin, * pFanins;
+    if ( Acb_ObjIsCi(p, iObj) )
+        return;
+    Vec_IntPush( vRes, iObj );
+    Acb_ObjForEachFaninFast( p, iObj, pFanins, Fanin, i )
+    {
+        assert( Vec_IntEntry(vRefs, Fanin) > 0 );
+        Vec_IntAddToEntry( vRefs, Fanin, -1 );
+        if ( Vec_IntEntry(vRefs, Fanin) == 0 )
+            Acb_NtkCollectDeref_rec( vRefs, p, Fanin, vRes );
+    }
+}
+Vec_Int_t * Acb_NtkCollectMffc( Acb_Ntk_t * p, Vec_Int_t * vObjsRefed, Vec_Int_t * vObjsDerefed )
+{
+    Vec_Int_t * vRes = Vec_IntAlloc( 100 );
+    Vec_Int_t * vRefs = Vec_IntStart( Acb_NtkObjNumMax(p) );
+    int i, iObj, Fanin, * pFanins;
+    Acb_NtkForEachObj( p, iObj )
+        Acb_ObjForEachFaninFast( p, iObj, pFanins, Fanin, i )
+            Vec_IntAddToEntry( vRefs, Fanin, 1 );
+    Acb_NtkForEachCo( p, iObj, i )
+        Vec_IntAddToEntry( vRefs, iObj, 1 );
+    if ( vObjsRefed )
+        Vec_IntForEachEntry( vObjsRefed, iObj, i )
+            Vec_IntAddToEntry( vRefs, iObj, 1 );
+    Vec_IntForEachEntry( vObjsDerefed, iObj, i )
+    {
+        if ( Acb_ObjIsCo(p, iObj) )
+            iObj = Acb_ObjFanin0(p, iObj);
+        if ( Vec_IntEntry(vRefs, iObj) != 0 )
+            Acb_NtkCollectDeref_rec( vRefs, p, iObj, vRes );
+    }
+    Vec_IntFree( vRefs );
+    Vec_IntUniqify( vRes );
+    return vRes;
+}
+
+Vec_Int_t * Acb_NamesToIds( Acb_Ntk_t * pNtk, Vec_Int_t * vNamesInv, Vec_Ptr_t * vNames )
+{
+    Vec_Int_t * vRes = Vec_IntAlloc( Vec_PtrSize(vNames) );
+    char * pName; int i;
+    Vec_PtrForEachEntry( char *, vNames, pName, i )
+    {
+        int NameId = Acb_NtkStrId(pNtk, pName);
+        int iObjId = 0;
+        if ( NameId < 1 )
+            printf( "Cannot find name \"%s\" in the network \"%s\".\n", pName, pNtk->pDesign->pName );
+        else
+            iObjId = Vec_IntEntry( vNamesInv, NameId );
+        Vec_IntPush( vRes, iObjId );
+    }
+    return vRes;
+}
+int Acb_NtkCollectMfsGates( char * pFileName, Vec_Ptr_t * vNamesRefed, Vec_Ptr_t * vNamesDerefed, int nGates[5] )
+{
+    Acb_Ntk_t * pNtkF        = Acb_VerilogSimpleRead( pFileName, NULL );
+    Vec_Int_t * vNamesInv    = Vec_IntInvert( &pNtkF->vObjName, 0 ) ;
+    Vec_Int_t * vObjsRefed   = Acb_NamesToIds( pNtkF, vNamesInv, vNamesRefed );
+    Vec_Int_t * vObjsDerefed = Acb_NamesToIds( pNtkF, vNamesInv, vNamesDerefed );
+    Vec_Int_t * vNodes       = Acb_NtkCollectMffc( pNtkF, vObjsRefed, vObjsDerefed );
+    int i, iObj, RetValue    = Vec_IntSize(vNodes);
+    Vec_IntFree( vNamesInv );
+    Vec_IntFree( vObjsRefed );
+    Vec_IntFree( vObjsDerefed );
+    for ( i = 0; i < 5; i++ )
+        nGates[i] = 0;
+    Vec_IntForEachEntry( vNodes, iObj, i )
+    {
+        int nFan = Acb_ObjFaninNum(pNtkF, iObj);
+        int Type = Acb_ObjType( pNtkF, iObj );
         if ( Type == ABC_OPER_CONST_F ) 
             nGates[0]++;
         else if ( Type == ABC_OPER_CONST_T ) 
@@ -219,31 +293,30 @@ int Acb_NtkNodeRef_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj, int nGates[5
         else
         {
             assert( nFan >= 2 );
-            nGates[4] += Acb_ObjFaninNum(p, iObj)-1;
+            nGates[4] += Acb_ObjFaninNum(pNtkF, iObj)-1;
         }
     }
-    Acb_ObjForEachFaninFast( p, iObj, pFanins, Fanin, i )
-    {
-        if ( Vec_IntEntry(vRefs, Fanin) == 0 )
-            Counter += Acb_NtkNodeRef_rec( vRefs, p, Fanin, nGates );
-        Vec_IntAddToEntry( vRefs, Fanin, 1 );
-    }
-    return Counter;
+    Vec_IntFree( vNodes );
+    Acb_ManFree( pNtkF->pDesign );
+    return RetValue;
 }
-int Acb_NtkFindMffcSize( Acb_Ntk_t * p, Vec_Int_t * vObjsRefed, Vec_Int_t * vObjsDerefed, int nGates[5] )
+Vec_Ptr_t * Acb_NtkReturnMfsGates( char * pFileName, Vec_Ptr_t * vNodes )
 {
-    Vec_Int_t * vRefs = Vec_IntStart( Acb_NtkObjNumMax(p) );
-    int i, iObj, Fanin, * pFanins, Count2 = 0;
-    Acb_NtkForEachObj( p, iObj )
-        Acb_ObjForEachFaninFast( p, iObj, pFanins, Fanin, i )
-            Vec_IntAddToEntry( vRefs, Fanin, 1 );
-    Vec_IntForEachEntry( vObjsRefed, iObj, i )
-        Vec_IntAddToEntry( vRefs, iObj, 1 );
-    Vec_IntForEachEntry( vObjsDerefed, iObj, i )
-        //if ( Vec_IntEntry(vRefs, iObj) != 0 || Acb_ObjIsCo(p, iObj) )
-            Count2 += Acb_NtkNodeDeref_rec( vRefs, p, iObj, nGates );
-    Vec_IntFree( vRefs );
-    return Count2;
+    Vec_Ptr_t * vMffc     = Vec_PtrAlloc( 100 );
+    Acb_Ntk_t * pNtkF     = Acb_VerilogSimpleRead( pFileName, NULL );
+    Vec_Int_t * vNamesInv = Vec_IntInvert( &pNtkF->vObjName, 0 ) ;
+    Vec_Int_t * vNodeObjs = Acb_NamesToIds( pNtkF, vNamesInv, vNodes );
+    Vec_Int_t * vNodeMffc = Acb_NtkCollectMffc( pNtkF, NULL, vNodeObjs );
+    int i, iObj;
+    Vec_IntForEachEntry( vNodeMffc, iObj, i )
+        Vec_PtrPush( vMffc, Abc_UtilStrsav( Acb_ObjNameStr(pNtkF, iObj) ) );
+//Vec_IntPrint( vNodeMffc );
+//Vec_PtrPrintNames( vMffc );
+    Vec_IntFree( vNodeMffc );
+    Vec_IntFree( vNodeObjs );
+    Vec_IntFree( vNamesInv );
+    Acb_ManFree( pNtkF->pDesign );
+    return vMffc;
 }
 
 /**Function*************************************************************
@@ -959,63 +1032,6 @@ int Abc_NtkExtract( char * pFileName0, char * pFileName1, int fUseXors, int fVer
   SeeAlso     []
 
 ***********************************************************************/
-void Acb_NtkFindNamesInPlaces( char * pBuffer, Vec_Int_t * vPlaces, Vec_Ptr_t * vPivots )
-{
-    int * pCounts = Abc_FrameReadGateCounts();
-    Vec_Ptr_t * vNames = Vec_PtrAlloc( 100 );
-    int i, k, iObj, Pos;
-    for ( i = 0; i < 5; i++ )
-        pCounts[i] = 0;
-    Vec_IntForEachEntryDouble( vPlaces, Pos, iObj, i )
-    {
-        int nFanins = 0;
-        char pLocal[1000], * pTemp, * pName, * pSpot;
-        char * pPivot = (char *)Vec_PtrEntry(vPivots, iObj);
-        for ( k = 0; k < 1000; k++ )
-        {
-            if ( pBuffer[Pos+k] == '\n' )
-            {
-                pLocal[k] = 0;
-                break;
-            }
-            else
-                pLocal[k] = pBuffer[Pos+k];
-        }
-        assert( k < 1000 );
-        pSpot = strstr( pLocal, pPivot );
-        if ( pSpot == NULL )
-        {
-            printf( "Cannot find location of signal \"%s\" in this line.\n", pPivot );
-            continue;
-        }
-        pTemp = strtok( pLocal, " \r\n\t,;()" );
-        while ( pTemp )
-        {
-            if ( !strcmp(pTemp, "1\'b0") )
-                pCounts[0]++;
-            else if ( !strcmp(pTemp, "1\'b1") )
-                pCounts[1]++;
-            else if ( !strcmp(pTemp, "buf") || !strcmp(pTemp, "assign") )
-                pCounts[2]++;
-            else if ( !strcmp(pTemp, "not") )
-                pCounts[3]++;
-            else if ( strcmp(pTemp, pPivot) && pTemp > pSpot )
-            {
-                nFanins++;
-                Vec_PtrForEachEntry( char *, vNames, pName, k )
-                    if ( !strcmp(pName, pTemp) )
-                        break;
-                if ( k == Vec_PtrSize(vNames) )
-                    Vec_PtrPush( vNames, Abc_UtilStrsav(pTemp) );
-            }
-            pTemp = strtok( NULL, " \r\n\t,;()" );
-        }
-        if ( nFanins > 1 )
-            pCounts[4] += nFanins-1;
-    }
-    //printf( "Found %d names\n", Vec_PtrSize(vNames) );
-    Abc_FrameSetSignalNames( vNames );
-}
 Vec_Int_t * Acb_NtkPlaces( char * pFileName, Vec_Ptr_t * vNames )
 {
     Vec_Int_t * vPlaces; int First = 1, Pos = -1, fComment = 0;
@@ -1057,7 +1073,7 @@ Vec_Int_t * Acb_NtkPlaces( char * pFileName, Vec_Ptr_t * vNames )
     ABC_FREE( pBuffer );
     return vPlaces;
 }
-void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames, int fNumber )
+void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames, int fNumber, int fSkipMffc )
 {
     int i, k, Prev = 0, Pos, Pos2, iObj;
     Vec_Int_t * vPlaces;
@@ -1075,16 +1091,32 @@ void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames,
         printf( "Cannot open input file \"%s\".\n", pFileNameIn );
         return;
     }
-    vPlaces = Acb_NtkPlaces( pFileNameIn, vNames );
-    Acb_NtkFindNamesInPlaces( pBuffer, vPlaces, vNames );
-    Vec_IntForEachEntryDouble( vPlaces, Pos, iObj, i )
+    if ( fSkipMffc )
     {
-        for ( k = Prev; k < Pos; k++ )
-            fputc( pBuffer[k], pFile );
-        fprintf( pFile, "// [t_%d = %s] //", iObj, (char *)Vec_PtrEntry(vNames, iObj) );
-        Prev = Pos;
+        Vec_Ptr_t * vMffcNames = Acb_NtkReturnMfsGates( pFileNameIn, vNames );
+        vPlaces = Acb_NtkPlaces( pFileNameIn, vMffcNames );
+        Vec_IntForEachEntryDouble( vPlaces, Pos, iObj, i )
+        {
+            for ( k = Prev; k < Pos; k++ )
+                fputc( pBuffer[k], pFile );
+            fprintf( pFile, "// MFFC %d = %s //", iObj, (char *)Vec_PtrEntry(vMffcNames, iObj) );
+            Prev = Pos;
+        }
+        Vec_IntFree( vPlaces );
+        Vec_PtrFreeFree( vMffcNames );
+    }
+    else
+    {
+        vPlaces = Acb_NtkPlaces( pFileNameIn, vNames );
+        Vec_IntForEachEntryDouble( vPlaces, Pos, iObj, i )
+        {
+            for ( k = Prev; k < Pos; k++ )
+                fputc( pBuffer[k], pFile );
+            fprintf( pFile, "// [t_%d = %s] //", iObj, (char *)Vec_PtrEntry(vNames, iObj) );
+            Prev = Pos;
+        }
+        Vec_IntFree( vPlaces );
     }
-    Vec_IntFree( vPlaces );
     pName = strstr(pBuffer, "endmodule");
     Pos2 = pName - pBuffer;
     for ( k = Prev; k < Pos2; k++ )
@@ -1238,12 +1270,12 @@ void Acb_Ntk4DumpWeights( char * pFileNameIn, Vec_Ptr_t * vObjNames, char * pFil
   SeeAlso     []
 
 ***********************************************************************/
-void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fRandom, int fUseWeights, int fInputs, int fVerbose, int fVeryVerbose )
+void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fRandom, int fUseWeights, int fInputs, int fSkipMffc, int fVerbose, int fVeryVerbose )
 {
-    extern int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fVerbose );
+    extern int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fSkipMffc, int fVerbose );
     extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fRandom, int fInputs, int fVerbose, int fVeryVerbose );
     char * pFileNames[4] = { pFileName[2], pFileName[1], fUseWeights ? (char *)"weights.txt" : NULL, pFileName[2] };
-    if ( Gia_Sim4Try( pFileName[0], pFileName[1], pFileName[2], nWords, nBeam, LevL, LevU, fOrder, fFancy, fUseBuf, fVerbose ) )
+    if ( Gia_Sim4Try( pFileName[0], pFileName[1], pFileName[2], nWords, nBeam, LevL, LevU, fOrder, fFancy, fUseBuf, fSkipMffc, fVerbose ) )
         Acb_NtkRunEco( pFileNames, 1, fRandom, fInputs, fVerbose, fVeryVerbose );
 } 
 
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 9ef8b6ff..a310972d 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -106,7 +106,7 @@ extern ABC_DLL void *          Abc_FrameReadManDec();
 extern ABC_DLL void *          Abc_FrameReadManDsd();           
 extern ABC_DLL void *          Abc_FrameReadManDsd2();           
 extern ABC_DLL Vec_Ptr_t *     Abc_FrameReadSignalNames();
-extern ABC_DLL int *           Abc_FrameReadGateCounts();
+extern ABC_DLL char *          Abc_FrameReadSpecName();
          
 extern ABC_DLL char *          Abc_FrameReadFlag( char * pFlag ); 
 extern ABC_DLL int             Abc_FrameIsFlagEnabled( char * pFlag );
@@ -150,6 +150,7 @@ extern ABC_DLL void            Abc_FrameSetStr( Vec_Str_t * vInv );
 extern ABC_DLL void            Abc_FrameSetJsonStrs( Abc_Nam_t * pStrs );
 extern ABC_DLL void            Abc_FrameSetJsonObjs( Vec_Wec_t * vObjs );
 extern ABC_DLL void            Abc_FrameSetSignalNames( Vec_Ptr_t * vNames );
+extern ABC_DLL void            Abc_FrameSetSpecName( char * pFileName );
 
 extern ABC_DLL int             Abc_FrameCheckPoConst( Abc_Frame_t * p, int iPoNum );
 
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 2743a90a..b7d76e93 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -68,7 +68,7 @@ void *      Abc_FrameReadManDsd()                            { return s_GlobalFr
 void *      Abc_FrameReadManDsd2()                           { return s_GlobalFrame->pManDsd2;     }
 char *      Abc_FrameReadFlag( char * pFlag )                { return Cmd_FlagReadByName( s_GlobalFrame, pFlag );   }
 Vec_Ptr_t * Abc_FrameReadSignalNames()                       { return s_GlobalFrame->vSignalNames; }
-int *       Abc_FrameReadGateCounts()                        { return s_GlobalFrame->pGateCounts;  }
+char *      Abc_FrameReadSpecName()                          { return s_GlobalFrame->pSpecName;    }
 
 int         Abc_FrameReadBmcFrames( Abc_Frame_t * p )        { return s_GlobalFrame->nFrames;      }               
 int         Abc_FrameReadProbStatus( Abc_Frame_t * p )       { return s_GlobalFrame->Status;       }               
@@ -105,6 +105,7 @@ void        Abc_FrameSetInv( Vec_Int_t * vInv )              { Vec_IntFreeP(&s_G
 void        Abc_FrameSetJsonStrs( Abc_Nam_t * pStrs )        { Abc_NamDeref( s_GlobalFrame->pJsonStrs ); s_GlobalFrame->pJsonStrs = pStrs; }
 void        Abc_FrameSetJsonObjs( Vec_Wec_t * vObjs )        { Vec_WecFreeP(&s_GlobalFrame->vJsonObjs ); s_GlobalFrame->vJsonObjs = vObjs; }
 void        Abc_FrameSetSignalNames( Vec_Ptr_t * vNames )    { if ( s_GlobalFrame->vSignalNames ) Vec_PtrFreeFree( s_GlobalFrame->vSignalNames ); s_GlobalFrame->vSignalNames = vNames; }
+void        Abc_FrameSetSpecName( char * pFileName )         { ABC_FREE( s_GlobalFrame->pSpecName ); s_GlobalFrame->pSpecName = pFileName; }
 
 int         Abc_FrameIsBatchMode()                           { return s_GlobalFrame ? s_GlobalFrame->fBatchMode : 0;              } 
 
@@ -236,6 +237,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     Vec_PtrFreeP( &p->vLTLProperties_global );
     if ( p->vSignalNames )
     Vec_PtrFreeFree( p->vSignalNames );
+    ABC_FREE( p->pSpecName );
     Abc_FrameDeleteAllNetworks( p );
     ABC_FREE( p->pDrivingCell );
     ABC_FREE( p->pCex2 );
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 9eaa03d1..e860878e 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -134,7 +134,7 @@ struct Abc_Frame_t_
     Vec_Ptr_t *     vPlugInComBinPairs;    // pairs of command and its binary name
     Vec_Ptr_t *     vLTLProperties_global; // related to LTL
     Vec_Ptr_t *     vSignalNames;  // temporary storage for signal names
-    int             pGateCounts[5];// temporary gate counts
+    char *          pSpecName;
     void *          pSave1; 
     void *          pSave2; 
     void *          pSave3; 
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index adc2f68e..bb9377bb 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -626,6 +626,26 @@ static inline void Vec_PtrCopy( Vec_Ptr_t * pDest, Vec_Ptr_t * pSour )
 
 /**Function*************************************************************
 
+  Synopsis    [Print names stored in the array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrPrintNames( Vec_Ptr_t * p )
+{
+    char * pName; int i;
+    printf( "Vector has %d entries: {", Vec_PtrSize(p) );
+    Vec_PtrForEachEntry( char *, p, pName, i )
+        printf( "%s ", pName );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []