Changes to several APIs.

8 files changed, 484 insertions, 81 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 9b5e5cdc..18544a73 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1255,6 +1255,7 @@ extern Gia_Man_t *         Gia_ManDupCofAll( Gia_Man_t * p, int nFanLim, int fVe
 extern void                Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSupp );
 extern void                Gia_ManCollectAnds_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes );
 extern void                Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes, Vec_Int_t * vLeaves );
+extern Vec_Int_t *         Gia_ManCollectAndsAll( Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManCollectNodesCis( Gia_Man_t * p, int * pNodes, int nNodes );
 extern int                 Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNodes );
 extern int                 Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes );
@@ -1697,6 +1698,7 @@ extern Vec_Int_t *         Gia_ManFirstFanouts( Gia_Man_t * p );
 extern int                 Gia_ManCheckSuppOverlap( Gia_Man_t * p, int iNode1, int iNode2 );
 extern int                 Gia_ManCountPisWithFanout( Gia_Man_t * p );
 extern int                 Gia_ManCountPosWithNonZeroDrivers( Gia_Man_t * p );
+extern void                Gia_ManUpdateCopy( Vec_Int_t * vCopy, Gia_Man_t * p );
 
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;
diff --git a/src/aig/gia/giaDfs.c b/src/aig/gia/giaDfs.c
index 12cae940..5cfe3b44 100644
--- a/src/aig/gia/giaDfs.c
+++ b/src/aig/gia/giaDfs.c
@@ -143,6 +143,26 @@ void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vN
 
 /**Function*************************************************************
 
+  Synopsis    [Collects support nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManCollectAndsAll( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj; int i;
+    Vec_Int_t * vNodes = Vec_IntAlloc( Gia_ManAndNum(p) );
+    Gia_ManForEachAnd( p, pObj, i )
+        Vec_IntPush( vNodes, i );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Counts the support size of the node.]
 
   Description []
diff --git a/src/aig/gia/giaSim4.c b/src/aig/gia/giaSim4.c
index ad0b7a21..04352761 100644
--- a/src/aig/gia/giaSim4.c
+++ b/src/aig/gia/giaSim4.c
@@ -41,8 +41,9 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_Sim4Try( char * pFileName0, char * pFileName1, int fVerbose )
+int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int fOrder, int fVerbose )
 {
+    return 0;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index eadc2a86..a753075f 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -2194,6 +2194,34 @@ int Gia_ManCountPosWithNonZeroDrivers( Gia_Man_t * p )
     return Count;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManUpdateCopy( Vec_Int_t * vCopy, Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, iLit;
+    Vec_IntForEachEntry( vCopy, iLit, i )
+    {
+        if ( iLit == -1 )
+            continue;
+        pObj = Gia_ManObj( p, Abc_Lit2Var(iLit) );
+        if ( !~pObj->Value )
+            Vec_IntWriteEntry( vCopy, i, -1 );
+        else
+            Vec_IntWriteEntry( vCopy, i, Abc_LitNotCond(pObj->Value, Abc_LitIsCompl(iLit)) );
+    }
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8d8f1ba4..11e847ce 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -4333,8 +4333,8 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( Abc_NtkNodeNum(pNtk) == 0 || Abc_NtkPiNum(pNtk) == 0 )
     {
-        Abc_Print( -1, "The network does not have internal nodes.\n" );
-        return 1;
+        Abc_Print( 0, "The network does not have internal nodes.\n" );
+        return 0;
     }
     if ( !Abc_NtkIsLogic(pNtk) )
     {
@@ -6933,13 +6933,17 @@ usage:
 ***********************************************************************/
 int Abc_CommandRunEco( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Acb_NtkRunEco( char * pFileNames[3], int fVerbose );
-    int c, fVerbose = 0;
+    extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose );
+    char * pFileNames[4] = {NULL};
+    int c, fCheck = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'c':
+            fCheck ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -6951,16 +6955,18 @@ int Abc_CommandRunEco( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 //    pArgvNew = argv + globalUtilOptind;
 //    nArgcNew = argc - globalUtilOptind;
-    if ( argc - globalUtilOptind != 3 )
+    if ( argc - globalUtilOptind < 2 || argc - globalUtilOptind > 3 )
     {
         Abc_Print( 1, "Expecting three file names on the command line.\n" );
         goto usage;
     }
-    Acb_NtkRunEco( argv + globalUtilOptind, fVerbose );
+    for ( c = 0; c < argc - globalUtilOptind; c++ )
+        pFileNames[c] = argv[globalUtilOptind+c];
+    Acb_NtkRunEco( pFileNames, fCheck, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: runeco <implementation> <specification> <weights> [-vh]\n" );
+    Abc_Print( -2, "usage: runeco [-cvh] <implementation> <specification> <weights>\n" );
     Abc_Print( -2, "\t         performs computation of patch functions during ECO,\n" );
     Abc_Print( -2, "\t         as described in the following paper: A. Q. Dao et al\n" );
     Abc_Print( -2, "\t         \"Efficient computation of ECO patch functions\", Proc. DAC\'18\n" );
@@ -6968,6 +6974,7 @@ usage:
     Abc_Print( -2, "\t         (currently only applicable to benchmarks from 2017 ICCAD CAD competition\n" );
     Abc_Print( -2, "\t         http://cad-contest-2017.el.cycu.edu.tw/Problem_A/default.html as follows:\n" );
     Abc_Print( -2, "\t         \"runeco unit1/F.v unit1/G.v unit1/weight.txt; cec -n out.v unit1/G.v\")\n" );
+    Abc_Print( -2, "\t-c     : toggle checking that the problem has a solution [default = %s]\n", fCheck? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -6988,6 +6995,7 @@ usage:
 int Abc_CommandRunGen( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Acb_NtkRunGen( char * pFileNames[2], int fVerbose );
+    char * pFileNames[4] = {NULL};
     int c, fVerbose = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@@ -7008,11 +7016,13 @@ int Abc_CommandRunGen( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Expecting two file names on the command line.\n" );
         goto usage;
     }
-    Acb_NtkRunGen( argv + globalUtilOptind, fVerbose );
+    for ( c = 0; c < 2; c++ )
+        pFileNames[c] = argv[globalUtilOptind+c];
+    Acb_NtkRunGen( pFileNames, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: rungen <file1> <file2> [-vh]\n" );
+    Abc_Print( -2, "usage: rungen [-vh] <file1> <file2>\n" );
     Abc_Print( -2, "\t         experimental command\n" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
@@ -7032,13 +7042,28 @@ usage:
 ***********************************************************************/
 int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Gia_Sim4Try( char * pFileName0, char * pFileName1, int fVerbose );
-    int c, fVerbose = 1;
+    extern void Acb_NtkRunSim( char * pFileName[4], int nWords, int fOrder, int fVerbose );
+    char * pFileNames[4] = {NULL, NULL, "out.v", NULL};
+    int c, fOrder = 0, nWords = 1, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Wovh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nWords < 0 )
+                goto usage;
+            break;
+        case 'o':
+            fOrder ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -7048,19 +7073,24 @@ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-    if ( argc - globalUtilOptind != 2 )
+    if ( argc - globalUtilOptind < 2 || argc - globalUtilOptind > 4 )
     {
-        Abc_Print( 1, "Expecting two file names on the command line.\n" );
+        Abc_Print( 1, "Expecting two or three file names on the command line.\n" );
         goto usage;
     }
-    Gia_Sim4Try( argv[globalUtilOptind+0], argv[globalUtilOptind+1], fVerbose );
+    Gia_ManRandom(1);
+    for ( c = 0; c < argc - globalUtilOptind; c++ )
+        pFileNames[c] = argv[globalUtilOptind+c];
+    Acb_NtkRunSim( pFileNames, nWords, fOrder, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: runsim <file1> <file2> [-vh]\n" );
-    Abc_Print( -2, "\t         experimental command\n" );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
+    Abc_Print( -2, "usage: runsim [-W] [-ovh] [-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-o       : toggle using a different node ordering [default = %s]\n", fOrder? "yes": "no" );
+    Abc_Print( -2, "\t-v       : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : print the command usage\n");
     return 1;
 }
 
diff --git a/src/base/acb/acbAbc.c b/src/base/acb/acbAbc.c
index 5fe7c7e3..9c2db080 100644
--- a/src/base/acb/acbAbc.c
+++ b/src/base/acb/acbAbc.c
@@ -177,7 +177,7 @@ Acb_Ntk_t * Acb_NtkFromNdr( char * pFileName, void * pModule, Abc_Nam_t * pNames
         ObjId  = Acb_ObjAlloc( pNtk, ABC_OPER_CI, 0, 0 );
         Vec_IntWriteEntry( vMap, NameId, ObjId );
         Acb_ObjSetName( pNtk, ObjId, NameId );
-        Acb_ObjSetWeight( pNtk, ObjId, vWeights ? Vec_IntEntry(vWeights, NameId) : 0 );
+        Acb_ObjSetWeight( pNtk, ObjId, vWeights ? Vec_IntEntry(vWeights, NameId) : 1 );
     }
     Ndr_ModForEachTarget( p, Mod, Obj )
     {
@@ -198,12 +198,14 @@ Acb_Ntk_t * Acb_NtkFromNdr( char * pFileName, void * pModule, Abc_Nam_t * pNames
     }
     Ndr_ModForEachNode( p, Mod, Obj )
     {
+        //char * pName;
         NameId = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT );
+        //pName = Abc_NamStr( pMan->pStrs, NameId );
         ObjId  = Vec_IntEntry( vMap, NameId );
         nArray = Ndr_ObjReadArray( p, Obj, NDR_INPUT, &pArray );
         for ( k = 0; k < nArray; k++ )
             Acb_ObjAddFanin( pNtk, ObjId, Vec_IntEntry(vMap, pArray[k]) );
-        Acb_ObjSetWeight( pNtk, ObjId, vWeights ? Vec_IntEntry(vWeights, NameId) : 0 );
+        Acb_ObjSetWeight( pNtk, ObjId, vWeights ? Vec_IntEntry(vWeights, NameId) : 1 );
     }
     Ndr_ModForEachPo( p, Mod, Obj )
     {
diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c
index f6fcf2b0..1708e51d 100644
--- a/src/base/acb/acbFunc.c
+++ b/src/base/acb/acbFunc.c
@@ -175,6 +175,14 @@ Abc_Nam_t * Acb_VerilogStartNames()
     }
     return pNames;
 }
+void Acb_VerilogRemoveComments ( char * pBuffer )
+{
+    char * pTemp;
+    for ( pTemp = pBuffer; *pTemp; pTemp++ )
+        if ( pTemp[0] == '/' && pTemp[1] == '/' )
+            while ( *pTemp && *pTemp != '\n' )
+                *pTemp++ = ' ';
+}
 Vec_Int_t * Acb_VerilogSimpleLex( char * pFileName, Abc_Nam_t * pNames )
 {
     Vec_Int_t * vBuffer = Vec_IntAlloc( 1000 );
@@ -182,11 +190,12 @@ Vec_Int_t * Acb_VerilogSimpleLex( char * pFileName, Abc_Nam_t * pNames )
     char * pToken;
     if ( pBuffer == NULL )
         return NULL;
-    pToken = strtok( pBuffer, "  \n\r()," );
+    Acb_VerilogRemoveComments( pBuffer );
+    pToken = strtok( pBuffer, "  \n\r\t()," );
     while ( pToken )
     {
         Vec_IntPush( vBuffer, Abc_NamStrFindOrAdd(pNames, pToken, NULL) );
-        pToken = strtok( NULL, "  \n\r(),;" );
+        pToken = strtok( NULL, "  \n\r\t(),;" );
     }
     ABC_FREE( pBuffer );
     return vBuffer;
@@ -204,7 +213,7 @@ void * Acb_VerilogSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames )
     Vec_Int_t * vWires   = Vec_IntAlloc(100);
     Vec_Int_t * vTypes   = Vec_IntAlloc(100);
     Vec_Int_t * vFanins  = Vec_IntAlloc(100);
-    Vec_Int_t * vCur = NULL;  
+    Vec_Int_t * vCur     = NULL;  
     int i, ModuleID, Token, Size, Count = 0;
     assert( Vec_IntEntry(vBuffer, 0) == ACB_MODULE );
     Vec_IntForEachEntryStart( vBuffer, Token, i, 2 )
@@ -221,9 +230,12 @@ void * Acb_VerilogSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames )
             vCur = vWires;
         else if ( Token >= ACB_BUF && Token <= ACB_XNOR )
         {
+            char * pToken = Abc_NamStr(pNames, Vec_IntEntry(vBuffer, i+1));
             Vec_IntPush( vTypes, Token );
             Vec_IntPush( vTypes, Vec_IntSize(vFanins) );
             vCur = vFanins;
+            if ( pToken[1] == 'z' && pToken[2] == '_' && pToken[3] == 'g' && pToken[4] == '_' )
+                i++;
         }
         else 
             Vec_IntPush( vCur, Token );
@@ -412,7 +424,7 @@ void Acb_VerilogSimpleWrite( Acb_Ntk_t * p, char * pFileName )
             assert( Acb_ObjType(p, iObj) == ABC_OPER_CONST_F || Acb_ObjType(p, iObj) == ABC_OPER_CONST_T );
             fprintf( pFile, "  %s (", Acb_Oper2Name( ABC_OPER_BIT_BUF ) );
             fprintf( pFile, " 1\'b%d", Acb_ObjType(p, iObj) == ABC_OPER_CONST_T );
-            fprintf( pFile, " );" );
+            fprintf( pFile, " );\n" );
         }
 
     fprintf( pFile, "\nendmodule\n\n" );
@@ -547,7 +559,7 @@ Vec_Int_t * Acb_NtkFindDivsCis( Acb_Ntk_t * p, Vec_Int_t * vSupp )
     printf( "Divisors are %d support variables (CIs in the TFO of the targets).\n", Vec_IntSize(vSupp) );
     return vDivs;
 }
-Vec_Int_t * Acb_NtkFindDivs( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Bit_t * vBlock )
+Vec_Int_t * Acb_NtkFindDivs( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Bit_t * vBlock, int fVerbose )
 {
     int fPrintWeights = 0;
     int nDivLimit = 3000;
@@ -589,8 +601,10 @@ Vec_Int_t * Acb_NtkFindDivs( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Bit_t * vBloc
             printf( "%d", (Vec_IntEntry(&p->vObjWeight, iObj) / 1) % 10 );
         printf( "\n" );
     }
+    if ( fVerbose )
     printf( "Reducing divisor set from %d to ", Vec_IntSize(vDivs) );
     Vec_IntShrink( vDivs, nDivLimit );
+    if ( fVerbose )
     printf( "%d.\n", Vec_IntSize(vDivs) );
     return vDivs;
 }
@@ -644,11 +658,15 @@ Vec_Int_t * Acb_NtkFindNodes( Acb_Ntk_t * p, Vec_Int_t * vRoots, Vec_Int_t * vDi
 ***********************************************************************/
 int Acb_ObjToGia( Gia_Man_t * pNew, Acb_Ntk_t * p, int iObj, Vec_Int_t * vTemp )
 {
+    //char * pName = Abc_NamStr( p->pDesign->pStrs, Acb_ObjName(p, iObj) );
     int * pFanin, iFanin, k, Type, Res;
     assert( !Acb_ObjIsCio(p, iObj) );
     Vec_IntClear( vTemp );
     Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, k )
+    {
+        assert( Acb_ObjCopy(p, iFanin) >= 0 );
         Vec_IntPush( vTemp, Acb_ObjCopy(p, iFanin) );
+    }
     Type = Acb_ObjType( p, iObj );
     if ( Type == ABC_OPER_CONST_F ) 
         return 0;
@@ -688,6 +706,7 @@ Gia_Man_t * Acb_NtkToGia( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Int_t * vNodes,
     Vec_Int_t * vFanins;
     int i, iObj;
     pNew = Gia_ManStart( 2 * Acb_NtkObjNum(p) + 1000 );
+    pNew->pName = Abc_UtilStrsav(Acb_NtkName(p));
     Gia_ManHashAlloc( pNew );
     Acb_NtkCleanObjCopies( p );
     // create primary inputs
@@ -1202,7 +1221,14 @@ Vec_Int_t * Acb_DerivePatchSupport( Cnf_Dat_t * pCnf, int iTar, int nTargets, in
             if ( TimeOut ) sat_solver_set_runtime_limit( pSat, TimeOut * CLOCKS_PER_SEC + Abc_Clock() );
             status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 );
             if ( TimeOut ) sat_solver_set_runtime_limit( pSat, 0 );
-            if ( status != l_False )
+            if ( status == l_True )
+            {
+                printf( "ECO does not exist.\n" );
+                sat_solver_delete( pSat );
+                Vec_IntFree( vSupp );
+                return NULL;
+            }
+            if ( status == l_Undef )
             {
                 printf( "Support computation timed out after %d sec.\n", TimeOut );
                 sat_solver_delete( pSat );
@@ -1789,12 +1815,12 @@ Vec_Str_t * Acb_GenerateInstance( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t *
 {
     int i, iObj;
     Vec_Str_t * vStr = Vec_StrAlloc( 100 );
-    Vec_StrAppend( vStr, "patch p0 (" );
+    Vec_StrAppend( vStr, "  patch p0 (" );
     Vec_IntForEachEntry( vTars, iObj, i )
         Vec_StrPrintF( vStr, "%s .%s(%s)", i ? ",":"", Acb_ObjNameStr(p, iObj), Acb_ObjNameStr(p, iObj) );
     Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i )
         Vec_StrPrintF( vStr, ", .%s(%s)", Acb_ObjNameStr(p, iObj), Acb_ObjNameStr(p, iObj) );
-    Vec_StrAppend( vStr, " );\n" );
+    Vec_StrAppend( vStr, " );\n\n" );
     Vec_StrPush( vStr, '\0' );
     return vStr;
 }
@@ -1880,7 +1906,7 @@ Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUs
             Vec_StrPrintF( vStr, "  %s (", Acb_Oper2Name( ABC_OPER_BIT_BUF ) );
             Vec_StrPrintF( vStr, " %s, ", (char *)Vec_PtrEntry(vNames, Vec_IntEntry(vGate, 1)) );
             Vec_StrPrintF( vStr, " 1\'b%d", Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T );
-            Vec_StrPrintF( vStr, " );" );
+            Vec_StrPrintF( vStr, " );\n" );
         }
     }
     Vec_StrAppend( vStr, "\nendmodule\n\n" );
@@ -1913,28 +1939,23 @@ void Acb_GenerateFilePatch( Vec_Str_t * p, char * pFileNamePatch )
 }
 void Acb_GenerateFileOut( Vec_Str_t * vPatchLine, char * pFileNameF, char * pFileNameOut, Vec_Str_t * vPatch )
 {
-    char * pBuffer = ABC_ALLOC( char, 10000 );
-    FILE * pFileIn, * pFileOut;
-    // input file
-    pFileIn = fopen( pFileNameF, "rb" );
-    if ( !pFileIn )
+    FILE * pFileOut;
+    char * pBuffer = Extra_FileReadContents( pFileNameF );
+    if ( pBuffer == NULL )
         return;
-    // output file
     pFileOut = fopen( pFileNameOut, "wb" );
-    if ( !pFileOut )
-        return;
-    // copy line by line
-    while ( fgets(pBuffer, 10000, pFileIn) )
+    if ( pFileOut )
     {
-        if ( strstr(pBuffer, "endmodule") )
-            fprintf( pFileOut, "\n%s", Vec_StrArray(vPatchLine) );
-        fputs( pBuffer, pFileOut );
+        char * pTemp = strstr( pBuffer, "endmodule" );
+        int nFirst = pTemp-pBuffer, nSecond = strlen(pBuffer) - nFirst;
+        int Value = fwrite( pBuffer, nFirst, 1, pFileOut );
+        fprintf( pFileOut, "\n%s", Vec_StrArray(vPatchLine) );
+        Value = fwrite( pBuffer+nFirst, nSecond, 1, pFileOut );
+        if ( vPatch )
+            fprintf( pFileOut, "\n%s\n", Vec_StrArray(vPatch) );
     }
-    if ( vPatch )
-        fprintf( pFileOut, "\n\n%s\n", Vec_StrArray(vPatch) );
-    fclose( pFileIn );
-    fclose( pFileOut );
     ABC_FREE( pBuffer );
+    fclose( pFileOut );
 }
 
 /**Function*************************************************************
@@ -2012,10 +2033,10 @@ Gia_Man_t * Acb_NtkEcoSynthesize( Gia_Man_t * p )
     }
     return pNew;
 }
-Cnf_Dat_t * Acb_NtkEcoCompute( Gia_Man_t * p, int iTar, int nTars )
+Cnf_Dat_t * Acb_NtkDeriveMiterCnf( Gia_Man_t * p, int iTar, int nTars, int fVerbose )
 {
     Gia_Man_t * pCof = Gia_ManDup( p );
-    Cnf_Dat_t * pCnf; int v, fVerbose = 1;
+    Cnf_Dat_t * pCnf; int v;
     for ( v = 0; v < iTar; v++ )
     {
         pCof = Gia_ManDupUniv( p = pCof, Gia_ManCiNum(pCof) - nTars + v );
@@ -2024,8 +2045,8 @@ Cnf_Dat_t * Acb_NtkEcoCompute( Gia_Man_t * p, int iTar, int nTars )
     }
     if ( fVerbose ) printf( "M_quo: " );
     if ( fVerbose ) Gia_ManPrintStats( pCof, NULL );
-    pCof = Acb_NtkEcoSynthesize( p = pCof );
-    Gia_ManStop( p );
+    //pCof = Acb_NtkEcoSynthesize( p = pCof );
+    //Gia_ManStop( p );
     if ( fVerbose ) printf( "M_syn: " );
     if ( fVerbose ) Gia_ManPrintStats( pCof, NULL );
     if ( 0 && iTar < nTars )
@@ -2113,7 +2134,7 @@ Gia_Man_t * Gia_ManInterOneInt( Gia_Man_t * pCof1, Gia_Man_t * pCof0, int Depth
         Gia_ManStop( pInter[m] );
     return pFinal;
 }
-Gia_Man_t * Acb_NtkEcoComputeInter2( Gia_Man_t * p, int iTar, int nTars )
+Gia_Man_t * Acb_NtkDeriveMiterCnfInter2( Gia_Man_t * p, int iTar, int nTars )
 {
 //    extern Gia_Man_t * Gia_ManInterOne( Gia_Man_t * pNtkOn, Gia_Man_t * pNtkOff, int fVerbose );
     extern Gia_Man_t * Abc_GiaSynthesizeInter( Gia_Man_t * p );
@@ -2154,7 +2175,7 @@ Gia_Man_t * Acb_NtkEcoComputeInter2( Gia_Man_t * p, int iTar, int nTars )
     //Gia_ManPrintStats( pInter, NULL );
     return pInter;
 }
-Gia_Man_t * Acb_NtkEcoComputeInter( Gia_Man_t * p, int iTar, int nTars )
+Gia_Man_t * Acb_NtkDeriveMiterCnfInter( Gia_Man_t * p, int iTar, int nTars )
 {
     Gia_Man_t * pCof1, * pCof = Gia_ManDup( p ); int v;
     for ( v = 0; v < iTar; v++ )
@@ -2271,7 +2292,7 @@ Vec_Ptr_t * Acb_TransformPatchFunctions( Vec_Ptr_t * vSops, Vec_Wec_t * vSupps,
   SeeAlso     []
 
 ***********************************************************************/
-int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF, int fCisOnly )
+int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4], int fCisOnly, int fCheck, int fVerbose )
 {
     extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp );
 
@@ -2286,7 +2307,7 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF,
     Vec_Int_t * vSuppF  = Acb_NtkFindSupp( pNtkF, vRoots );
     Vec_Int_t * vSuppG  = Acb_NtkFindSupp( pNtkG, vRoots );
     Vec_Int_t * vSupp   = Vec_IntTwoMerge( vSuppF, vSuppG );
-    Vec_Int_t * vDivs   = fCisOnly ? Acb_NtkFindDivsCis( pNtkF, vSupp ) : Acb_NtkFindDivs( pNtkF, vSupp, vBlock );
+    Vec_Int_t * vDivs   = fCisOnly ? Acb_NtkFindDivsCis( pNtkF, vSupp ) : Acb_NtkFindDivs( pNtkF, vSupp, vBlock, fVerbose );
     Vec_Int_t * vNodesF = Acb_NtkFindNodes( pNtkF, vRoots, vDivs );
     Vec_Int_t * vNodesG = Acb_NtkFindNodes( pNtkG, vRoots, NULL );
 
@@ -2309,21 +2330,24 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF,
     char * pSop = NULL;
     int i, Res;
 
-    printf( "The number of targets = %d.\n", nTargets );
-
-    printf( "NtkF:  " );
-    Gia_ManPrintStats( pGiaF, NULL );
-    printf( "NtkG:  " );
-    Gia_ManPrintStats( pGiaG, NULL );
-    printf( "Miter: " );
-    Gia_ManPrintStats( pGiaM, NULL );
+    if ( fVerbose )
+    {
+        printf( "The number of targets = %d.\n", nTargets );
+
+        printf( "NtkF:  " );
+        Gia_ManPrintStats( pGiaF, NULL );
+        printf( "NtkG:  " );
+        Gia_ManPrintStats( pGiaG, NULL );
+        printf( "Miter: " );
+        Gia_ManPrintStats( pGiaM, NULL );
+    }
 
     // check that the problem has a solution
-    if ( 0 )//fCisOnly )
+    if ( fCheck )//fCisOnly )
     {
         int Lit, status;
         sat_solver * pSat;
-        pCnf = Acb_NtkEcoCompute( pGiaM, nTargets, nTargets );
+        pCnf = Acb_NtkDeriveMiterCnf( pGiaM, nTargets, nTargets, fVerbose );
         pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
         Cnf_DataFree( pCnf );
         // add output clause
@@ -2350,7 +2374,7 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF,
             vSupp = Vec_IntStartNatural( Vec_IntSize(vDivs) );
             printf( "Target %d has support with %d variables.\n", i, Vec_IntSize(vSupp) );
 
-            pOne = Acb_NtkEcoComputeInter( pGiaM, i, nTargets );
+            pOne = Acb_NtkDeriveMiterCnfInter( pGiaM, i, nTargets );
             printf( "Tar%02d: ", i );
             Gia_ManPrintStats( pOne, NULL );
 
@@ -2363,12 +2387,11 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF,
         }
         else
         {
-            pCnf = Acb_NtkEcoCompute( pGiaM, i, nTargets );
+            pCnf = Acb_NtkDeriveMiterCnf( pGiaM, i, nTargets, fVerbose );
 //            vSupp = Acb_DerivePatchSupportS( pCnf, i, nTargets, Vec_IntSize(vDivs), vDivs, pNtkF, NULL, TimeOut );
             vSupp = Acb_DerivePatchSupport( pCnf, i, nTargets, Vec_IntSize(vDivs), vDivs, pNtkF, vSuppOld, TimeOut );
             if ( vSupp == NULL )
             {
-                Vec_IntFree( vSuppOld );
                 Cnf_DataFree( pCnf );
                 RetValue = 0;
                 goto cleanup;
@@ -2383,7 +2406,6 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF,
             Cnf_DataFree( pCnf );
             if ( pSop == NULL )
             {
-                Vec_IntFree( vSuppOld );
                 RetValue = 0;
                 goto cleanup;
             }
@@ -2405,7 +2427,6 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF,
         Vec_IntAppend( Vec_WecPushLevel(vSupps), vSupp );
         Vec_IntFree( vSupp );
     }
-    Vec_IntFree( vSuppOld );
 
     // make sure the function is UNSAT
     printf( "\n" );
@@ -2443,8 +2464,9 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF,
     Acb_PrintPatch( pNtkF, vDivs, vUsed, clk );
 
     // generate output files
-    Acb_GenerateFilePatch( vPatch, "patch.v" );
-    Acb_GenerateFileOut( vInst, pFileNameF, "out.v", vPatch );
+    if ( pFileName[3] == NULL ) Acb_GenerateFilePatch( vPatch, "patch.v" );
+    Acb_GenerateFileOut( vInst, pFileName[0], pFileName[3] ? pFileName[3] : "out.v", vPatch );
+    printf( "Finished dumping resulting file \"%s\".\n\n", pFileName[3] ? pFileName[3] : "out.v" );
     //Gia_AigerWrite( pGiaG, "test.aig", 0, 0, 0 );
 cleanup:
     // cleanup
@@ -2460,9 +2482,9 @@ cleanup:
 
     Vec_PtrFreeFree( vSops );
     Vec_WecFree( vSupps );
-
-    if ( vFuncs ) Vec_PtrFreeFree( vFuncs );
+    Vec_IntFree( vSuppOld );
     Vec_IntFreeP( &vUsed );
+    if ( vFuncs ) Vec_PtrFreeFree( vFuncs );
 
     Gia_ManStop( pGiaF );
     Gia_ManStop( pGiaG );
@@ -2511,7 +2533,7 @@ void Acb_NtkTestRun2( char * pFileNames[3], int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-void Acb_NtkRunEco( char * pFileNames[3], int fVerbose )
+void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose )
 {
     Acb_Ntk_t * pNtkF = Acb_VerilogSimpleRead( pFileNames[0], pFileNames[2] );
     Acb_Ntk_t * pNtkG = Acb_VerilogSimpleRead( pFileNames[1], NULL );
@@ -2528,11 +2550,11 @@ void Acb_NtkRunEco( char * pFileNames[3], int fVerbose )
 
     Acb_IntallLibrary();
 
-    if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames[0], 0 ) )
+    if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 0, fCheck, fVerbose ) )
     {
-        printf( "General ECO computation timed out. Trying inputs only.\n\n" );
-        if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames[0], 1 ) )
-            printf( "Input-only ECO computation also timed out.\n\n" );
+        printf( "General computation timed out. Trying inputs only.\n\n" );
+        if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 1, fCheck, fVerbose ) )
+            printf( "Input-only computation also timed out.\n\n" );
     }
 
     Acb_ManFree( pNtkF->pDesign );
diff --git a/src/base/acb/acbUtil.c b/src/base/acb/acbUtil.c
index 2d56a553..ecf84bb6 100644
--- a/src/base/acb/acbUtil.c
+++ b/src/base/acb/acbUtil.c
@@ -470,6 +470,304 @@ void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp
     Vec_IntClear( &p->vSuppOld );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Derive AIG for one network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acb_NtkFindNodes2_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vNodes )
+{
+    int * pFanin, iFanin, i;
+    if ( Acb_ObjSetTravIdCur(p, iObj) )
+        return;
+    if ( Acb_ObjIsCi(p, iObj) )
+        return;
+    Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, i )
+        Acb_NtkFindNodes2_rec( p, iFanin, vNodes );
+    assert( !Acb_ObjIsCo(p, iObj) );
+    Vec_IntPush( vNodes, iObj );
+}
+Vec_Int_t * Acb_NtkFindNodes2( Acb_Ntk_t * p )
+{
+    int i, iObj;
+    Vec_Int_t * vNodes = Vec_IntAlloc( 1000 );
+    Acb_NtkIncTravId( p );
+    Acb_NtkForEachCo( p, iObj, i )
+        Acb_NtkFindNodes2_rec( p, Acb_ObjFanin(p, iObj, 0), vNodes );
+    return vNodes;
+}
+int Acb_ObjToGia2( Gia_Man_t * pNew, Acb_Ntk_t * p, int iObj, Vec_Int_t * vTemp )
+{
+    //char * pName = Abc_NamStr( p->pDesign->pStrs, Acb_ObjName(p, iObj) );
+    int * pFanin, iFanin, k, Type, Res;
+    assert( !Acb_ObjIsCio(p, iObj) );
+    Vec_IntClear( vTemp );
+    Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, k )
+    {
+        assert( Acb_ObjCopy(p, iFanin) >= 0 );
+        Vec_IntPush( vTemp, Acb_ObjCopy(p, iFanin) );
+    }
+    Type = Acb_ObjType( p, iObj );
+    if ( Type == ABC_OPER_CONST_F ) 
+        return 0;
+    if ( Type == ABC_OPER_CONST_T ) 
+        return 1;
+    if ( Type == ABC_OPER_BIT_BUF ) 
+        return Vec_IntEntry(vTemp, 0);
+    if ( Type == ABC_OPER_BIT_INV ) 
+        return Abc_LitNot( Vec_IntEntry(vTemp, 0) );
+    if ( Type == ABC_OPER_BIT_AND || Type == ABC_OPER_BIT_NAND )
+    {
+        Res = 1;
+        Vec_IntForEachEntry( vTemp, iFanin, k )
+            Res = Gia_ManAppendAnd2( pNew, Res, iFanin );
+        return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NAND );
+    }
+    if ( Type == ABC_OPER_BIT_OR || Type == ABC_OPER_BIT_NOR )
+    {
+        Res = 0;
+        Vec_IntForEachEntry( vTemp, iFanin, k )
+            Res = Gia_ManAppendOr2( pNew, Res, iFanin );
+        return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NOR );
+    }
+    if ( Type == ABC_OPER_BIT_XOR || Type == ABC_OPER_BIT_NXOR )
+    {
+        Res = 0;
+        Vec_IntForEachEntry( vTemp, iFanin, k )
+            Res = Gia_ManAppendXor2( pNew, Res, iFanin );
+        return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NXOR );
+    }
+    assert( 0 );
+    return -1;
+}
+Gia_Man_t * Acb_NtkToGia2( Acb_Ntk_t * p )
+{
+    Gia_Man_t * pNew, * pOne;
+    Vec_Int_t * vFanins, * vNodes;
+    int i, iObj;
+    pNew = Gia_ManStart( 2 * Acb_NtkObjNum(p) + 1000 );
+    pNew->pName = Abc_UtilStrsav(Acb_NtkName(p));
+    Acb_NtkCleanObjCopies( p );
+    Acb_NtkForEachCi( p, iObj, i )
+        Acb_ObjSetCopy( p, iObj, Gia_ManAppendCi(pNew) );
+    vFanins = Vec_IntAlloc( 4 );
+    vNodes  = Acb_NtkFindNodes2( p );
+    Vec_IntForEachEntry( vNodes, iObj, i )
+        Acb_ObjSetCopy( p, iObj, Acb_ObjToGia2(pNew, p, iObj, vFanins) );
+    Vec_IntFree( vNodes );
+    Vec_IntFree( vFanins );
+    Acb_NtkForEachCo( p, iObj, i )
+        Gia_ManAppendCo( pNew, Acb_ObjCopy(p, Acb_ObjFanin(p, iObj, 0)) );
+    pNew = Gia_ManCleanup( pOne = pNew );
+    Gia_ManUpdateCopy( &p->vObjCopy, pOne );
+    Gia_ManStop( pOne );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Acb_NtkCollectCopies( Acb_Ntk_t * p, Gia_Man_t * pGia, Vec_Ptr_t ** pvNodesR )
+{
+    int i, iObj, iLit;
+    Vec_Int_t * vObjs   = Acb_NtkFindNodes2( p );
+    Vec_Int_t * vNodes  = Vec_IntAlloc( Acb_NtkObjNum(p) );
+    Vec_Ptr_t * vNodesR = Vec_PtrStart( Gia_ManObjNum(pGia) );
+    Vec_IntForEachEntry( vObjs, iObj, i )
+        if ( (iLit = Acb_ObjCopy(p, iObj)) >= 0 && Gia_ObjIsAnd(Gia_ManObj(pGia, Abc_Lit2Var(iLit))) )
+        {
+            if ( Vec_PtrEntry(vNodesR, Abc_Lit2Var(iLit)) == NULL )
+            {
+                Vec_PtrWriteEntry( vNodesR, Abc_Lit2Var(iLit), Abc_UtilStrsav(Acb_ObjNameStr(p, iObj)) );
+                Vec_IntPush( vNodes, Abc_Lit2Var(iLit) );
+            }
+        }
+    Vec_IntFree( vObjs );
+    Vec_IntSort( vNodes, 0 );
+    *pvNodesR = vNodesR;
+    return vNodes;
+}
+Vec_Int_t * Acb_NtkCollectUser( Acb_Ntk_t * p, Vec_Ptr_t * vUser )
+{
+    char * pTemp; int i;
+    Vec_Int_t * vRes = Vec_IntAlloc( Vec_PtrSize(vUser) );
+    Vec_Int_t * vMap = Vec_IntStart( Abc_NamObjNumMax(Acb_NtkNam(p)) );
+    Acb_NtkForEachNode( p, i )
+        if ( Acb_ObjName(p, i) > 0 )
+            Vec_IntWriteEntry( vMap, Acb_ObjName(p, i), Acb_ObjCopy(p, i) );
+    Vec_PtrForEachEntry( char *, vUser, pTemp, i )
+        if ( Acb_NtkStrId(p, pTemp) < Vec_IntSize(vMap) )
+        {
+            int iLit = Vec_IntEntry( vMap, Acb_NtkStrId(p, pTemp) );
+            assert( iLit > 0 );
+            //printf( "Obj = %3d  Name = %3d  Copy = %3d\n", i, Acb_NtkStrId(p, pTemp), iLit );
+            Vec_IntPush( vRes, Abc_Lit2Var(iLit) );
+        }
+    assert( Vec_IntSize(vRes) == Vec_PtrSize(vUser) );
+    Vec_IntFree( vMap );
+    Vec_IntUniqify( vRes );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Acb_NtkExtract( char * pFileName0, char * pFileName1, int fVerbose, 
+                    Gia_Man_t ** ppGiaF, Gia_Man_t ** ppGiaG, Vec_Int_t ** pvNodes, Vec_Ptr_t ** pvNodesR )
+{
+    extern Acb_Ntk_t * Acb_VerilogSimpleRead( char * pFileName, char * pFileNameW );
+    Acb_Ntk_t * pNtkF = Acb_VerilogSimpleRead( pFileName0, NULL );
+    Acb_Ntk_t * pNtkG = Acb_VerilogSimpleRead( pFileName1, NULL );
+    int RetValue = 0;
+    if ( pNtkF && pNtkG )
+    {
+        Gia_Man_t * pGiaF = Acb_NtkToGia2( pNtkF );
+        Gia_Man_t * pGiaG = Acb_NtkToGia2( pNtkG );
+        assert( Acb_NtkCiNum(pNtkF) == Acb_NtkCiNum(pNtkG) );
+        assert( Acb_NtkCoNum(pNtkF) == Acb_NtkCoNum(pNtkG) );
+        *ppGiaF  = pGiaF;
+        *ppGiaG  = pGiaG;
+        *pvNodes = Acb_NtkCollectCopies( pNtkF, pGiaF, pvNodesR );
+        RetValue = 1;
+    }
+    if ( pNtkF->pDesign ) Acb_ManFree( pNtkF->pDesign );
+    if ( pNtkG->pDesign ) Acb_ManFree( pNtkG->pDesign );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Acb_NtkPlaces( char * pFileName, Vec_Ptr_t * vNames )
+{
+    Vec_Int_t * vPlaces; int First = 1, Pos = -1;
+    char * pTemp, * pBuffer = Extra_FileReadContents( pFileName );
+    char * pLimit = pBuffer + strlen(pBuffer);
+    if ( pBuffer == NULL )
+        return NULL;
+    vPlaces = Vec_IntAlloc( Vec_PtrSize(vNames) );
+    for ( pTemp = pBuffer; *pTemp; pTemp++ )
+    {
+        if ( *pTemp == '\n' )
+            Pos = pTemp - pBuffer + 1;
+        else if ( *pTemp == '(' )
+        {
+            if ( First )
+                First = 0;
+            else
+            {
+                char * pToken = strtok( pTemp+1, "  \n\r\t" );
+                char * pName; int i;
+                Vec_PtrForEachEntry( char *, vNames, pName, i )
+                    if ( !strcmp(pName, pToken) )
+                        Vec_IntPushTwo( vPlaces, Pos, i );
+                pTemp = pToken + strlen(pToken);
+                while ( *pTemp == 0 )
+                    pTemp++;
+                assert( pTemp < pLimit );
+            }
+        }
+    }
+    assert( Vec_IntSize(vPlaces) == 2*Vec_PtrSize(vNames) );
+    ABC_FREE( pBuffer );
+    return vPlaces;
+}
+void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames )
+{
+    int i, k, Prev = 0, Pos, Pos2, iObj;
+    Vec_Int_t * vPlaces;
+    char * pName, * pBuffer;
+    FILE * pFile = fopen( pFileNameOut, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open output file \"%s\".\n", pFileNameOut );
+        return;
+    }
+    pBuffer = Extra_FileReadContents( pFileNameIn );
+    if ( pBuffer == NULL )
+    {
+        fclose( pFile );
+        printf( "Cannot open input file \"%s\".\n", pFileNameIn );
+        return;
+    }
+    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 );
+    pName = strstr(pBuffer, "endmodule");
+    Pos2 = pName - pBuffer;
+    for ( k = Prev; k < Pos2; k++ )
+        fputc( pBuffer[k], pFile );
+    fprintf( pFile, "\n\n" );
+    fprintf( pFile, "  wire " );
+    Vec_PtrForEachEntry( char *, vNames, pName, i )
+        fprintf( pFile, " t_%d%s", i, i==Vec_PtrSize(vNames)-1 ? ";" : "," );
+    fprintf( pFile, "\n\n" );
+    Vec_PtrForEachEntry( char *, vNames, pName, i )
+        fprintf( pFile, "  buf( %s, t_%d );\n", pName, i );
+    fprintf( pFile, "\n" );
+    for ( k = Pos2; pBuffer[k]; k++ )
+        fputc( pBuffer[k], pFile );
+    ABC_FREE( pBuffer );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acb_NtkRunSim( char * pFileName[4], int nWords, int fOrder, int fVerbose )
+{
+    extern int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int fOrder, int fVerbose );
+    extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose );
+    char * pFileNames[4] = { pFileName[2], pFileName[1], NULL, pFileName[2] };
+    if ( Gia_Sim4Try( pFileName[0], pFileName[1], pFileName[2], nWords, fOrder, fVerbose ) )
+        Acb_NtkRunEco( pFileNames, 0, fVerbose );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////