Version abc70428

15 files changed, 1091 insertions, 47 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 98942ca3..3b309b43 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -330,7 +330,7 @@ static inline bool        Abc_NtkIsComb( Abc_Ntk_t * pNtk )          { return Ab
 static inline bool        Abc_NtkHasOnlyLatchBoxes(Abc_Ntk_t * pNtk ){ return Abc_NtkLatchNum(pNtk) == Abc_NtkBoxNum(pNtk); }
 
 // creating simple objects
-extern inline Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
+extern        Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
 static inline Abc_Obj_t * Abc_NtkCreatePi( Abc_Ntk_t * pNtk )        { return Abc_NtkCreateObj( pNtk, ABC_OBJ_PI );         }
 static inline Abc_Obj_t * Abc_NtkCreatePo( Abc_Ntk_t * pNtk )        { return Abc_NtkCreateObj( pNtk, ABC_OBJ_PO );         }
 static inline Abc_Obj_t * Abc_NtkCreateBi( Abc_Ntk_t * pNtk )        { return Abc_NtkCreateObj( pNtk, ABC_OBJ_BI );         }
@@ -417,8 +417,8 @@ static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj )          { return Ab
 static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ){ return Abc_ObjNotCond( Abc_ObjFanin(pObj,i)->pCopy, Abc_ObjFaninC(pObj,i) );  }
 static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );    }
 static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) );    }
-static inline Abc_Obj_t * Abc_ObjChild0Data( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pData, Abc_ObjFaninC0(pObj) );    }
-static inline Abc_Obj_t * Abc_ObjChild1Data( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pData, Abc_ObjFaninC1(pObj) );    }
+static inline Abc_Obj_t * Abc_ObjChild0Data( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( (Abc_Obj_t *)Abc_ObjFanin0(pObj)->pData, Abc_ObjFaninC0(pObj) );    }
+static inline Abc_Obj_t * Abc_ObjChild1Data( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( (Abc_Obj_t *)Abc_ObjFanin1(pObj)->pData, Abc_ObjFaninC1(pObj) );    }
 static inline Hop_Obj_t * Abc_ObjChild0Equiv( Abc_Obj_t * pObj )     { return Hop_NotCond( Abc_ObjFanin0(pObj)->pEquiv, Abc_ObjFaninC0(pObj) );      }
 static inline Hop_Obj_t * Abc_ObjChild1Equiv( Abc_Obj_t * pObj )     { return Hop_NotCond( Abc_ObjFanin1(pObj)->pEquiv, Abc_ObjFaninC1(pObj) );      }
 
@@ -452,17 +452,17 @@ static inline int         Abc_LatchInit( Abc_Obj_t * pLatch )        { assert(Ab
 
 // global BDDs of the nodes
 static inline void *      Abc_NtkGlobalBdd( Abc_Ntk_t * pNtk )          { return (void *)Vec_PtrEntry(pNtk->vAttrs, VEC_ATTR_GLOBAL_BDD);             }
-static inline DdManager * Abc_NtkGlobalBddMan( Abc_Ntk_t * pNtk )       { return (DdManager *)Vec_AttMan( Abc_NtkGlobalBdd(pNtk) );                   }
-static inline DdNode **   Abc_NtkGlobalBddArray( Abc_Ntk_t * pNtk )     { return (DdNode **)Vec_AttArray( Abc_NtkGlobalBdd(pNtk) );                   }
-static inline DdNode *    Abc_ObjGlobalBdd( Abc_Obj_t * pObj )          { return (DdNode *)Vec_AttEntry( Abc_NtkGlobalBdd(pObj->pNtk), pObj->Id );    }
-static inline void        Abc_ObjSetGlobalBdd( Abc_Obj_t * pObj, DdNode * bF )   { Vec_AttWriteEntry( Abc_NtkGlobalBdd(pObj->pNtk), pObj->Id, bF );   }
+static inline DdManager * Abc_NtkGlobalBddMan( Abc_Ntk_t * pNtk )       { return (DdManager *)Vec_AttMan( (Vec_Att_t *)Abc_NtkGlobalBdd(pNtk) );                   }
+static inline DdNode **   Abc_NtkGlobalBddArray( Abc_Ntk_t * pNtk )     { return (DdNode **)Vec_AttArray( (Vec_Att_t *)Abc_NtkGlobalBdd(pNtk) );                   }
+static inline DdNode *    Abc_ObjGlobalBdd( Abc_Obj_t * pObj )          { return (DdNode *)Vec_AttEntry( (Vec_Att_t *)Abc_NtkGlobalBdd(pObj->pNtk), pObj->Id );    }
+static inline void        Abc_ObjSetGlobalBdd( Abc_Obj_t * pObj, DdNode * bF )   { Vec_AttWriteEntry( (Vec_Att_t *)Abc_NtkGlobalBdd(pObj->pNtk), pObj->Id, bF );   }
 
 // MV variables of the nodes
 static inline void *      Abc_NtkMvVar( Abc_Ntk_t * pNtk )              { return Vec_PtrEntry(pNtk->vAttrs, VEC_ATTR_MVVAR);                          }
-static inline void *      Abc_NtkMvVarMan( Abc_Ntk_t * pNtk )           { return Abc_NtkMvVar(pNtk)? Vec_AttMan( Abc_NtkMvVar(pNtk) ) : NULL;         }
-static inline void *      Abc_ObjMvVar( Abc_Obj_t * pObj )              { return Abc_NtkMvVar(pObj->pNtk)? Vec_AttEntry( Abc_NtkMvVar(pObj->pNtk), pObj->Id ) : NULL; }
+static inline void *      Abc_NtkMvVarMan( Abc_Ntk_t * pNtk )           { return Abc_NtkMvVar(pNtk)? Vec_AttMan( (Vec_Att_t *)Abc_NtkMvVar(pNtk) ) : NULL;         }
+static inline void *      Abc_ObjMvVar( Abc_Obj_t * pObj )              { return Abc_NtkMvVar(pObj->pNtk)? Vec_AttEntry( (Vec_Att_t *)Abc_NtkMvVar(pObj->pNtk), pObj->Id ) : NULL; }
 static inline int         Abc_ObjMvVarNum( Abc_Obj_t * pObj )           { return (Abc_NtkMvVar(pObj->pNtk) && Abc_ObjMvVar(pObj))? *((int*)Abc_ObjMvVar(pObj)) : 2;   }
-static inline void        Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_AttWriteEntry( Abc_NtkMvVar(pObj->pNtk), pObj->Id, pV );                }
+static inline void        Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_AttWriteEntry( (Vec_Att_t *)Abc_NtkMvVar(pObj->pNtk), pObj->Id, pV );                }
 
 // outputs the runtime in seconds
 #define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 39d7cb2b..1e0fed0c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -329,6 +329,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Abc_NtkPrint256();
 //    Kit_TruthCountMintermsPrecomp();
 //    Kit_DsdPrecompute4Vars();
+
+    Dar_LibStart();
 } 
 
 /**Function*************************************************************
@@ -344,6 +346,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
 ***********************************************************************/
 void Abc_End()
 {
+    Dar_LibStop();
+
     Abc_NtkFraigStoreClean();
 //    Rwt_Man4ExplorePrint();
 }
@@ -6034,13 +6038,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 //    Abc_NtkCompareSupports( pNtk );
 //    Abc_NtkCompareCones( pNtk );
-
+/*
     {
         extern Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int fVerbose );
         Vec_Vec_t * vParts;
         vParts = Abc_NtkPartitionSmart( pNtk, 1 );
         Vec_VecFree( vParts );
     }
+*/
+//    Abc_Ntk4VarTable( pNtk );
+//    Dat_NtkGenerateArrays( pNtk );
 
     return 0;
 
@@ -7677,7 +7684,8 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fUseInv;
     int fExdc;
     int fVerbose;
-    extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose );
+    int fVeryVerbose;
+    extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose, int fVeryVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -7687,8 +7695,9 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     fUseInv   = 1;
     fExdc     = 0;
     fVerbose  = 0;
+    fVeryVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ievh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ievwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7701,6 +7710,9 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'v':
             fVerbose ^= 1;
             break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -7724,7 +7736,7 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     // modify the current network
-    if ( !Abc_NtkFraigSweep( pNtk, fUseInv, fExdc, fVerbose ) )
+    if ( !Abc_NtkFraigSweep( pNtk, fUseInv, fExdc, fVerbose, fVeryVerbose ) )
     {
         fprintf( pErr, "Sweeping has failed.\n" );
         return 1;
@@ -7732,10 +7744,11 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: fraig_sweep [-evh]\n" );
+    fprintf( pErr, "usage: fraig_sweep [-evwh]\n" );
     fprintf( pErr, "\t        performs technology-dependent sweep\n" );
     fprintf( pErr, "\t-e    : toggle functional sweeping using EXDC [default = %s]\n", fExdc? "yes": "no" );
     fprintf( pErr, "\t-v    : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-w    : prints equivalence class information [default = %s]\n", fVeryVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -8284,7 +8297,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVerbose;
     int c;
     extern Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fSwitching, int fVerbose );
-    extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose );
+    extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose, int fVeryVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -8375,7 +8388,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     if ( fSweep )
-        Abc_NtkFraigSweep( pNtkRes, 0, 0, 0 );
+        Abc_NtkFraigSweep( pNtkRes, 0, 0, 0, 0 );
 
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -10346,11 +10359,12 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nPartSize;
     int nConfLimit;
     int nInsLimit;
+    int fPartition;
 
     extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit );
     extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose );
     extern void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nPartSize, int fVerbose );
-
+    extern void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -10363,8 +10377,9 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     nPartSize  = 0;
     nConfLimit = 10000;   
     nInsLimit  = 0;
+    fPartition = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "TCIPsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "TCIPpsvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -10412,6 +10427,9 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nPartSize < 0 ) 
                 goto usage;
             break;
+        case 'p':
+            fPartition ^= 1;
+            break;
         case 's':
             fSat ^= 1;
             break;
@@ -10429,7 +10447,9 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
 
     // perform equivalence checking
-    if ( nPartSize )
+    if ( fPartition )
+        Abc_NtkCecFraigPartAuto( pNtk1, pNtk2, nSeconds, fVerbose );
+    else if ( nPartSize )
         Abc_NtkCecFraigPart( pNtk1, pNtk2, nSeconds, nPartSize, fVerbose );
     else if ( fSat )
         Abc_NtkCecSat( pNtk1, pNtk2, nConfLimit, nInsLimit );
@@ -10445,12 +10465,13 @@ usage:
         strcpy( Buffer, "unused" );
     else
         sprintf( Buffer, "%d", nPartSize );
-    fprintf( pErr, "usage: cec [-T num] [-C num] [-I num] [-P num] [-svh] <file1> <file2>\n" );
+    fprintf( pErr, "usage: cec [-T num] [-C num] [-I num] [-P num] [-psvh] <file1> <file2>\n" );
     fprintf( pErr, "\t         performs combinational equivalence checking\n" );
     fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
     fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
     fprintf( pErr, "\t-I num : limit on the number of clause inspections [default = %d]\n", nInsLimit );
     fprintf( pErr, "\t-P num : partition size for multi-output networks [default = %s]\n", Buffer );
+    fprintf( pErr, "\t-p     : toggle automatic partitioning [default = %s]\n", fPartition? "yes": "no" );
     fprintf( pErr, "\t-s     : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
     fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
new file mode 100644
index 00000000..0863061b
--- /dev/null
+++ b/src/base/abci/abcDar.c
@@ -0,0 +1,154 @@
+/**CFile****************************************************************
+
+  FileName    [abcDar.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [DAG-aware rewriting.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcDar.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "dar.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk );
+static Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkAig;
+    Dar_Man_t * pMan;//, * pTemp;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // convert to the AIG manager
+    pMan = Abc_NtkToDar( pNtk );
+    if ( pMan == NULL )
+        return NULL;
+    if ( !Dar_ManCheck( pMan ) )
+    {
+        printf( "Abc_NtkDar: AIG check has failed.\n" );
+        Dar_ManStop( pMan );
+        return NULL;
+    }
+    // perform balance
+    Dar_ManPrintStats( pMan );
+//    Dar_ManDumpBlif( pMan, "aig_temp.blif" );
+    pMan->pPars = Dar_ManDefaultParams();
+    Dar_ManRewrite( pMan );
+    Dar_ManPrintStats( pMan );
+    // convert from the AIG manager
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    if ( pNtkAig == NULL )
+        return NULL;
+    Dar_ManStop( pMan );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkAig ) )
+    {
+        printf( "Abc_NtkDar: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkAig );
+        return NULL;
+    }
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the AIG manager into ABC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk )
+{
+    Dar_Man_t * pMan;
+    Abc_Obj_t * pObj;
+    int i;
+    // create the manager
+    pMan = Dar_ManStart( Abc_NtkNodeNum(pNtk) );
+    // transfer the pointers to the basic nodes
+    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Dar_ManConst1(pMan);
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Dar_ObjCreatePi(pMan);
+    // perform the conversion of the internal nodes (assumes DFS ordering)
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Dar_And( pMan, (Dar_Obj_t *)Abc_ObjChild0Copy(pObj), (Dar_Obj_t *)Abc_ObjChild1Copy(pObj) );
+    // create the POs
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Dar_ObjCreatePo( pMan, (Dar_Obj_t *)Abc_ObjChild0Copy(pObj) );
+    Dar_ManCleanup( pMan );
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the AIG manager into ABC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtk, Dar_Man_t * pMan )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Ntk_t * pNtkNew;
+    Dar_Obj_t * pObj;
+    int i;
+    // perform strashing
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // transfer the pointers to the basic nodes
+    Dar_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
+    Dar_ManForEachPi( pMan, pObj, i )
+        pObj->pData = Abc_NtkCi(pNtkNew, i);
+    // rebuild the AIG
+    vNodes = Dar_ManDfs( pMan );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Dar_ObjChild0Copy(pObj), (Abc_Obj_t *)Dar_ObjChild1Copy(pObj) );
+    Vec_PtrFree( vNodes );
+    // connect the PO nodes
+    Dar_ManForEachPo( pMan, pObj, i )
+        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Dar_ObjChild0Copy(pObj) );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcDsdRes.c b/src/base/abci/abcDsdRes.c
index 50c624d7..83e1c241 100644
--- a/src/base/abci/abcDsdRes.c
+++ b/src/base/abci/abcDsdRes.c
@@ -994,6 +994,73 @@ If_Obj_t * Abc_LutIfManMap_New_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit
 
 /**Function*************************************************************
 
+  Synopsis    [Find the best cofactoring variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
+int Abc_LutFindBestCofactoring( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
+{
+    Kit_DsdNtk_t * pNtk0, * pNtk1, * pTemp;
+//    Kit_DsdObj_t * pRoot;
+    unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) };
+    unsigned i, * pTruth;
+    int MaxBlock
+        Verbose = 0;
+    int RetValue = 0;
+
+    if ( fVerbose )
+    {
+        printf( "Function: " );
+//        Extra_PrintBinary( stdout, pTruth, (1 << nVars) ); 
+        Extra_PrintHexadecimal( stdout, pTruth, nVars ); 
+        printf( "\n" );
+        Kit_DsdPrint( stdout, pNtk );
+    }
+    for ( i = 0; i < nVars; i++ )
+    {
+        Kit_TruthCofactor0New( pCofs2[0], pTruth, nVars, i );
+        pNtk0 = Kit_DsdDecompose( pCofs2[0], nVars );
+        pNtk0 = Kit_DsdExpand( pTemp = pNtk0 );
+        Kit_DsdNtkFree( pTemp );
+
+        if ( fVerbose )
+        {
+            printf( "Cof%d0: ", i );
+            Kit_DsdPrint( stdout, pNtk0 );
+        }
+
+        Kit_TruthCofactor1New( pCofs2[1], pTruth, nVars, i );
+        pNtk1 = Kit_DsdDecompose( pCofs2[1], nVars );
+        pNtk1 = Kit_DsdExpand( pTemp = pNtk1 );
+        Kit_DsdNtkFree( pTemp );
+
+        if ( fVerbose )
+        {
+            printf( "Cof%d1: ", i );
+            Kit_DsdPrint( stdout, pNtk1 );
+        }
+
+        if ( Kit_DsdCheckVar4Dec2( pNtk0, pNtk1 ) )
+            RetValue = 1;
+
+        Kit_DsdNtkFree( pNtk0 );
+        Kit_DsdNtkFree( pNtk1 );
+    }
+    if ( fVerbose )
+        printf( "\n" );
+
+    return RetValue;
+    
+}
+*/
+/**Function*************************************************************
+
   Synopsis    [Prepares the mapping manager.]
 
   Description []
@@ -1220,6 +1287,7 @@ clk = clock();
         pTruth = Abc_LutCutTruth( p, pCut );
 p->timeTruth += clock() - clk;
 
+
 /*
         // evaluate the result of decomposition        
         Result = Kit_DsdEval( pTruth, pCut->nLeaves, 3 );
@@ -1247,6 +1315,18 @@ p->timeEval += clock() - clk;
             continue;
         }
 */
+  
+/*        
+        if ( pCut->nLeaves > 6 && pCut->nLeaves < 12 && Kit_DsdNonDsdSizeMax(pDsdNtk) == pCut->nLeaves )
+        {
+//            Abc_NtkPrintMeasures( pTruth, pCut->nLeaves );
+//            Kit_DsdTestCofs( pDsdNtk, pTruth );
+
+//            Abc_NtkPrintOneDecomp( pTruth, pCut->nLeaves );
+            Abc_NtkPrintOneDec( pTruth, pCut->nLeaves );
+        }
+*/
+
         if ( p->pPars->fVeryVerbose )
         {
 //            Extra_PrintHexadecimal( stdout, pTruth, pCut->nLeaves ); printf( "\n" );
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index d3779277..b878091b 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -525,6 +525,8 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
     if ( pParams->fUseRewriting && Abc_NtkNodeNum(pNtk) > 500 )
     {
         pParams->fUseRewriting = 0;
+        pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
+        Abc_NtkDelete( pNtkTemp );
         Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
         pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
         Abc_NtkDelete( pNtkTemp );
diff --git a/src/base/abci/abcMeasure.c b/src/base/abci/abcMeasure.c
new file mode 100644
index 00000000..6604a0c4
--- /dev/null
+++ b/src/base/abci/abcMeasure.c
@@ -0,0 +1,478 @@
+/**CFile****************************************************************
+
+  FileName    [abc_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintMeasures( unsigned * pTruth, int nVars )
+{
+    unsigned uCofs[10][32];
+    int i, k, nOnes;
+
+    // total pairs
+    nOnes =  Kit_TruthCountOnes( uCofs[0], nVars );
+    printf( "Total = %d.\n", nOnes * ((1 << nVars) - nOnes) );
+
+    // print measures for individual variables
+    for ( i = 0; i < nVars; i++ )
+    {
+        Kit_TruthUniqueNew( uCofs[0], pTruth, nVars, i );
+        nOnes = Kit_TruthCountOnes( uCofs[0], nVars );
+        printf( "%7d ", nOnes );
+    }
+    printf( "\n" );
+
+    // consider pairs
+    for ( i = 0; i < nVars; i++ )
+    for ( k = 0; k < nVars; k++ )
+    {
+        if ( i == k )
+        {
+            printf( "        " );
+            continue;
+        }
+        Kit_TruthCofactor0New( uCofs[0], pTruth, nVars, i );
+        Kit_TruthCofactor1New( uCofs[1], pTruth, nVars, i );
+
+        Kit_TruthCofactor0New( uCofs[2], uCofs[0], nVars, k ); // 00
+        Kit_TruthCofactor1New( uCofs[3], uCofs[0], nVars, k ); // 01
+        Kit_TruthCofactor0New( uCofs[4], uCofs[1], nVars, k ); // 10
+        Kit_TruthCofactor1New( uCofs[5], uCofs[1], nVars, k ); // 11
+
+        Kit_TruthAndPhase( uCofs[6], uCofs[2], uCofs[5], nVars, 0, 1 ); // 00  & 11'
+        Kit_TruthAndPhase( uCofs[7], uCofs[2], uCofs[5], nVars, 1, 0 ); // 00' & 11
+        Kit_TruthAndPhase( uCofs[8], uCofs[3], uCofs[4], nVars, 0, 1 ); // 01  & 10'
+        Kit_TruthAndPhase( uCofs[9], uCofs[3], uCofs[4], nVars, 1, 0 ); // 01' & 10
+
+        nOnes = Kit_TruthCountOnes( uCofs[6], nVars ) + 
+                Kit_TruthCountOnes( uCofs[7], nVars ) + 
+                Kit_TruthCountOnes( uCofs[8], nVars ) + 
+                Kit_TruthCountOnes( uCofs[9], nVars );
+
+        printf( "%7d ", nOnes );
+        if ( k == nVars - 1 )
+            printf( "\n" );
+    }
+    printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_Ntk4VarObjPrint_rec( Abc_Obj_t * pObj )
+{
+    if ( pObj == Abc_AigConst1(pObj->pNtk) )
+    {
+        printf( "1" );
+        return;
+    }
+    if ( Abc_ObjIsPi(pObj) )
+    {
+        printf( "%c", pObj->Id - 1 + 'a' );
+        return;
+    }
+
+    printf( "(" );
+    Abc_Ntk4VarObjPrint_rec( Abc_ObjFanin0(pObj) );
+    if ( Abc_ObjFaninC0(pObj) )
+        printf( "\'" );
+    Abc_Ntk4VarObjPrint_rec( Abc_ObjFanin1(pObj) );
+    if ( Abc_ObjFaninC1(pObj) )
+        printf( "\'" );
+    printf( ")" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Abc_Ntk4VarObj( Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pObj;
+    unsigned uTruth0, uTruth1;
+    int i;
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        uTruth0 = (unsigned)(Abc_ObjFanin0(pObj)->pCopy);
+        uTruth1 = (unsigned)(Abc_ObjFanin1(pObj)->pCopy);
+        if ( Abc_ObjFaninC0(pObj) )
+            uTruth0 = ~uTruth0;
+        if ( Abc_ObjFaninC1(pObj) )
+            uTruth1 = ~uTruth1;
+        pObj->pCopy = (void *)(uTruth0 & uTruth1);
+    }
+    return uTruth0 & uTruth1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_Ntk4VarTable( Abc_Ntk_t * pNtk )
+{
+    static unsigned u4VarTruths[4] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00 };
+    static unsigned u4VarTts[222] = {
+        0x0000, 0x0001, 0x0003, 0x0006, 0x0007, 0x000f, 0x0016, 0x0017, 0x0018, 0x0019, 
+        0x001b, 0x001e, 0x001f, 0x003c, 0x003d, 0x003f, 0x0069, 0x006b, 0x006f, 0x007e, 
+        0x007f, 0x00ff, 0x0116, 0x0117, 0x0118, 0x0119, 0x011a, 0x011b, 0x011e, 0x011f, 
+        0x012c, 0x012d, 0x012f, 0x013c, 0x013d, 0x013e, 0x013f, 0x0168, 0x0169, 0x016a, 
+        0x016b, 0x016e, 0x016f, 0x017e, 0x017f, 0x0180, 0x0181, 0x0182, 0x0183, 0x0186, 
+        0x0187, 0x0189, 0x018b, 0x018f, 0x0196, 0x0197, 0x0198, 0x0199, 0x019a, 0x019b, 
+        0x019e, 0x019f, 0x01a8, 0x01a9, 0x01aa, 0x01ab, 0x01ac, 0x01ad, 0x01ae, 0x01af, 
+        0x01bc, 0x01bd, 0x01be, 0x01bf, 0x01e8, 0x01e9, 0x01ea, 0x01eb, 0x01ee, 0x01ef, 
+        0x01fe, 0x033c, 0x033d, 0x033f, 0x0356, 0x0357, 0x0358, 0x0359, 0x035a, 0x035b, 
+        0x035e, 0x035f, 0x0368, 0x0369, 0x036a, 0x036b, 0x036c, 0x036d, 0x036e, 0x036f, 
+        0x037c, 0x037d, 0x037e, 0x03c0, 0x03c1, 0x03c3, 0x03c5, 0x03c6, 0x03c7, 0x03cf, 
+        0x03d4, 0x03d5, 0x03d6, 0x03d7, 0x03d8, 0x03d9, 0x03db, 0x03dc, 0x03dd, 0x03de, 
+        0x03fc, 0x0660, 0x0661, 0x0662, 0x0663, 0x0666, 0x0667, 0x0669, 0x066b, 0x066f, 
+        0x0672, 0x0673, 0x0676, 0x0678, 0x0679, 0x067a, 0x067b, 0x067e, 0x0690, 0x0691, 
+        0x0693, 0x0696, 0x0697, 0x069f, 0x06b0, 0x06b1, 0x06b2, 0x06b3, 0x06b4, 0x06b5, 
+        0x06b6, 0x06b7, 0x06b9, 0x06bd, 0x06f0, 0x06f1, 0x06f2, 0x06f6, 0x06f9, 0x0776, 
+        0x0778, 0x0779, 0x077a, 0x077e, 0x07b0, 0x07b1, 0x07b4, 0x07b5, 0x07b6, 0x07bc, 
+        0x07e0, 0x07e1, 0x07e2, 0x07e3, 0x07e6, 0x07e9, 0x07f0, 0x07f1, 0x07f2, 0x07f8, 
+        0x0ff0, 0x1668, 0x1669, 0x166a, 0x166b, 0x166e, 0x167e, 0x1681, 0x1683, 0x1686, 
+        0x1687, 0x1689, 0x168b, 0x168e, 0x1696, 0x1697, 0x1698, 0x1699, 0x169a, 0x169b, 
+        0x169e, 0x16a9, 0x16ac, 0x16ad, 0x16bc, 0x16e9, 0x177e, 0x178e, 0x1796, 0x1798, 
+        0x179a, 0x17ac, 0x17e8, 0x18e7, 0x19e1, 0x19e3, 0x19e6, 0x1bd8, 0x1be4, 0x1ee1, 
+        0x3cc3, 0x6996
+    };
+    int Counters[222] = {0};
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj;
+    unsigned uTruth;
+    int i, k, Count = 0;
+
+    unsigned short * puCanons = NULL;
+    unsigned char * puMap = NULL;
+    Extra_Truth4VarNPN( &puCanons, NULL, NULL, &puMap );
+
+    // set elementary truth tables
+    assert( Abc_NtkPiNum(pNtk) == 4 );
+    Abc_AigConst1(pNtk)->pCopy = (void *)0xFFFFFFFF;
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        pObj->pCopy = (void *)u4VarTruths[i];
+
+    // create truth tables
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
+        if ( Vec_PtrSize(vNodes) == 0 )
+            uTruth = (unsigned)Abc_ObjFanin0(pObj)->pCopy;
+        else
+            uTruth = Abc_Ntk4VarObj( vNodes );
+
+        if ( (uTruth & 0xFFFF) < (~uTruth & 0xFFFF) )
+            uTruth = uTruth & 0xFFFF;
+        else
+            uTruth = ~uTruth & 0xFFFF;
+
+        for ( k = 0; k < 222; k++ )
+            if ( u4VarTts[k] == uTruth )
+                break;
+        if ( k == 222 )
+            continue;
+/*
+//        if ( uTruth == 1725 )
+        if ( k == 96 )
+        {
+            printf( "%d : ", Vec_PtrSize(vNodes) );
+            Abc_Ntk4VarObjPrint_rec( Abc_ObjFanin0(pObj) );
+            printf( "\n" );
+        }
+*/
+        Counters[k]++;
+
+//        Counters[ puMap[uTruth & 0xFFFF] ]++;
+        Vec_PtrFree( vNodes );
+    }
+    free( puCanons );
+    free( puMap );
+
+    Count = 0;
+    for ( k = 0; k < 222; k++ )
+    {
+        printf( "%d/%x/%d ", k, u4VarTts[k], Counters[k] );
+        Count += Counters[k];
+    }
+    printf( " Total = %d\n", Count );
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if there are no more than 2 unique cofactors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkPrintOneDecompCheckCofList( unsigned * uCofs, int nCofs )
+{
+    int i, Ind = -1;
+    assert( nCofs > 2 );
+    for ( i = 1; i < nCofs; i++ )
+    {
+        if ( uCofs[i] == uCofs[0] )
+            continue;
+        if ( Ind == -1 )
+        {
+            Ind = i;
+            continue;
+        }
+        if ( uCofs[i] == uCofs[Ind] )
+            continue;
+        return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks all cofactors with the given mask.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkPrintOneDecompCheck( unsigned * uCofs, int nCofs, unsigned uMask )
+{
+    unsigned pCofs[32][32];
+    int nCofNums[32] = {0};
+    int uMasks[32];
+    int nGroups = 0;
+    int i, k;
+    for ( i = 0; i < nCofs; i++ )
+    {
+        // find group of this cof
+        for ( k = 0; k < nGroups; k++ )
+            if ( (int)(i & uMask) == uMasks[k] )
+                break;
+        if ( k == nGroups )
+        {
+            uMasks[k] = (i & uMask);
+            nGroups++;
+        }
+        // save cof in the group
+        pCofs[k][ nCofNums[k]++ ] = uCofs[i];
+        assert( nCofNums[k] <= 32 );
+        assert( nGroups <= 32 );
+    }
+    // check the groups
+    for ( i = 0; i < nGroups; i++ )
+        if ( !Abc_NtkPrintOneDecompCheckCofList(pCofs[i], nCofNums[i]) )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintOneDecomp_rec( unsigned * uCofs, int nCofs, int nVars, unsigned uMask, int * pBestSize, unsigned * puBestMask )
+{
+    unsigned uMaskNew;
+    int v, last, Counter = 0;
+    // find the last variable in the mask
+    for ( v = 0; v < nVars; v++ )
+        if ( uMask & (1<<v) )
+        {
+            last = v;
+            Counter++;
+        }
+    if ( Counter > 3 )
+        return;
+    // try adding one variable after the last
+    for ( v = last + 1; v < nVars; v++ )
+    {
+        uMaskNew = uMask | (1 << v);
+        if ( !Abc_NtkPrintOneDecompCheck( uCofs, nCofs, uMaskNew ) )
+            continue;
+        if ( *pBestSize < Counter + 1 )
+        {
+            *pBestSize = Counter + 1;
+            *puBestMask = uMaskNew;
+        }
+        // try other masks
+        Abc_NtkPrintOneDecomp_rec( uCofs, nCofs, nVars, uMaskNew, pBestSize, puBestMask );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintOneDecomp( unsigned * pTruth, int nVars )
+{
+    int BoundSet = 6;
+    unsigned uCofs[64], uMask, uBestMask = 0;
+    int i, nCofs, nMints, nMintShift, BestSize = 1;
+
+    assert( nVars >  BoundSet );
+    assert( nVars <= BoundSet + 5 ); // at most 5 variable cofactors
+
+    // collect the cofactors
+    nCofs = (1 << BoundSet);
+    nMints = (1 << (nVars-BoundSet));
+    nMintShift = 0;
+    uMask = Kit_CubeMask( nMints );
+    for ( i = 0; i < nCofs; i++ )
+    {
+        uCofs[i] = (pTruth[nMintShift/32] >> (nMintShift % 32)) & uMask;
+        nMintShift += nMints;
+    }
+
+    // try removing variables
+    for ( i = 0; i < BoundSet; i++ )
+        Abc_NtkPrintOneDecomp_rec( uCofs, nCofs, nVars, (1 << i), &BestSize, &uBestMask );
+
+    printf( "Best size = %d  ", BestSize );
+    printf( "Best mask = " );
+    Extra_PrintBinary( stdout, &uBestMask, nVars );
+    printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintOneDec( unsigned * pTruth, int nVars )
+{
+    unsigned uCof[(1<<11)], * pOut = uCof, * pIn = pTruth, * pTemp;
+    int nDiffs[16];
+    int Order[16];
+    int i, fChange, Temp, Counter;
+
+    // find the ordering
+    for ( i = 0; i < nVars; i++ )
+    {
+        Kit_TruthUniqueNew( uCof, pTruth, nVars, i );
+        nDiffs[i] = Kit_TruthCountOnes( uCof, nVars );
+        Order[i] = i;
+    }
+
+    // permute truth table to least active variable first
+    Counter = 0;
+    do {
+        fChange = 0;
+        for ( i = 0; i < nVars-1; i++ )
+        {
+            if ( nDiffs[i] <= nDiffs[i+1] )
+                continue;
+            fChange = 1;
+            Counter++;
+
+            Temp = nDiffs[i];
+            nDiffs[i] = nDiffs[i+1];
+            nDiffs[i+1] = Temp;
+
+            Temp = Order[i];
+            Order[i] = Order[i+1];
+            Order[i+1] = Temp;
+
+            Extra_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
+            pTemp = pIn; pIn = pOut; pOut = pTemp;
+        }
+    } while ( fChange );
+
+    // swap if it was moved an even number of times
+    if ( Counter & 1 )
+        Extra_TruthCopy( pOut, pIn, nVars );
+
+    // call the decomposition
+    Abc_NtkPrintOneDecomp( pTruth, nVars );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
index 14e33c36..748868de 100644
--- a/src/base/abci/abcPart.c
+++ b/src/base/abci/abcPart.c
@@ -74,9 +74,9 @@ Vec_Ptr_t * Abc_NtkPartitionCollectSupps( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Int_t * vOne )
+int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vPartsAll, int nPartSizeLimit, Vec_Int_t * vOne )
 {
-    Vec_Int_t * vPartSupp;
+    Vec_Int_t * vPartSupp, * vPart;
     double Attract, Repulse, Cost, CostBest;
     int i, nCommon, iBest;
     iBest = -1;
@@ -84,6 +84,11 @@ int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Int_t * vOne )
     Vec_PtrForEachEntry( vPartSuppsAll, vPartSupp, i )
     {
         nCommon = Vec_IntTwoCountCommon( vPartSupp, vOne );
+        if ( nCommon == 0 )
+            continue;
+        vPart = Vec_PtrEntry( vPartsAll, i );
+        if ( nPartSizeLimit > 0 && Vec_IntSize(vPart) > nPartSizeLimit )
+            continue;
         if ( nCommon == Vec_IntSize(vOne) )
             return i;
         Attract = 1.0 * nCommon / Vec_IntSize(vOne);
@@ -143,17 +148,20 @@ void Abc_NtkPartitionPrint( Abc_Ntk_t * pNtk, Vec_Ptr_t * vPartsAll, Vec_Ptr_t *
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll )
+void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll, int nPartSizeLimit )
 {
     Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
     int i, iPart;
 
+    if ( nPartSizeLimit == 0 )
+        nPartSizeLimit = 200;
+
     // pack smaller partitions into larger blocks
     iPart = 0;
     vPart = vPartSupp = NULL;
     Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
     {
-        if ( Vec_IntSize(vOne) < 200 )
+        if ( Vec_IntSize(vOne) < nPartSizeLimit )
         {
             if ( vPartSupp == NULL )
             {
@@ -169,7 +177,7 @@ void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll )
                 Vec_IntFree( vTemp );
                 Vec_IntFree( Vec_PtrEntry(vPartsAll, i) );
             }
-            if ( Vec_IntSize(vPartSupp) < 200 )
+            if ( Vec_IntSize(vPartSupp) < nPartSizeLimit )
                 continue;
         }
         else
@@ -212,7 +220,7 @@ void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int fVerbose )
+Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nPartSizeLimit, int fVerbose )
 {
     Vec_Ptr_t * vSupps, * vPartsAll, * vPartsAll2, * vPartSuppsAll, * vPartPtr;
     Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
@@ -235,7 +243,7 @@ clk = clock();
         // get the output number
         iOut = Vec_IntPop(vOne);
         // find closely matching part
-        iPart = Abc_NtkPartitionSmartFindPart( vPartSuppsAll, vOne );
+        iPart = Abc_NtkPartitionSmartFindPart( vPartSuppsAll, vPartsAll, nPartSizeLimit, vOne );
         if ( iPart == -1 )
         {
             // create new partition
@@ -280,7 +288,7 @@ clk = clock();
 
     // compact small partitions
 //    Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll );
-    Abc_NtkPartitionCompact( vPartsAll, vPartSuppsAll );
+    Abc_NtkPartitionCompact( vPartsAll, vPartSuppsAll, nPartSizeLimit );
     if ( fVerbose )
     Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll );
 if ( fVerbose )
@@ -668,7 +676,7 @@ Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams )
     // perform partitioning
     assert( Abc_NtkIsStrash(pNtk) );
 //    vParts = Abc_NtkPartitionNaive( pNtk, 20 );
-    vParts = Abc_NtkPartitionSmart( pNtk, 0 );
+    vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 );
 
     Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
 
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 43ddb4fd..c4ec68f3 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -26,7 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static void           Abc_NtkFraigSweepUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
-static stmm_table *   Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose );
+static stmm_table *   Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose, int fVeryVerbose );
 static void           Abc_NtkFraigTransform( Abc_Ntk_t * pNtk, stmm_table * tEquiv, int fUseInv, bool fVerbose );
 static void           Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv, int fVerbose );
 static void           Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv, int fVerbose );
@@ -54,7 +54,7 @@ static void           Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pF
   SeeAlso     []
 
 ***********************************************************************/
-bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose )
+bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose, int fVeryVerbose )
 {
     Fraig_Params_t Params;
     Abc_Ntk_t * pNtkAig;
@@ -100,9 +100,11 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose )
         else
             Abc_NtkFraigSweepUsingExdc( pMan, pNtk );
     }
+    // assign levels to the nodes of the network
+    Abc_NtkLevel( pNtk );
 
     // collect the classes of equivalent nets
-    tEquiv = Abc_NtkFraigEquiv( pNtk, fUseInv, fVerbose );
+    tEquiv = Abc_NtkFraigEquiv( pNtk, fUseInv, fVerbose, fVeryVerbose );
 
     // transform the network into the equivalent one
     Abc_NtkFraigTransform( pNtk, tEquiv, fUseInv, fVerbose );
@@ -113,7 +115,11 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose )
     Abc_NtkDelete( pNtkAig );
 
     // cleanup the dangling nodes
-    Abc_NtkCleanup( pNtk, fVerbose );
+    if ( Abc_NtkHasMapping(pNtk) )
+        Abc_NtkCleanup( pNtk, fVerbose );
+    else
+        Abc_NtkSweep( pNtk, fVerbose );
+
     // check
     if ( !Abc_NtkCheck( pNtk ) )
     {
@@ -175,7 +181,7 @@ void Abc_NtkFraigSweepUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose )
+stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose, int fVeryVerbose )
 {
     Abc_Obj_t * pList, * pNode, * pNodeAig;
     Fraig_Node_t * gNode;
@@ -225,22 +231,22 @@ stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose )
         // count nodes in the non-trival classes
         for ( pNode = pList; pNode; pNode = pNode->pNext )
             Counter++;
-/*
-        if ( fVerbose )
+
+        if ( fVeryVerbose )
         {
             printf( "Class %2d : {", c );
             for ( pNode = pList; pNode; pNode = pNode->pNext )
             {
                 pNode->pCopy = NULL;
                 printf( " %s", Abc_ObjName(pNode) );
-                if ( pNode->fPhase )  printf( "(*)" );
+                printf( "(%c)", pNode->fPhase? '-' : '+' );
+                printf( "(%d)", pNode->Level );
             }
             printf( " }\n" );
             c++;
         }
-*/
     }
-    if ( fVerbose )
+    if ( fVerbose || fVeryVerbose )
     {
         printf( "Sweeping stats for network \"%s\":\n", pNtk->pName );
         printf( "Internal nodes = %d. Different functions (up to compl) = %d.\n", Abc_NtkNodeNum(pNtk), stmm_count(tStrash2Net) );
@@ -268,8 +274,6 @@ void Abc_NtkFraigTransform( Abc_Ntk_t * pNtk, stmm_table * tEquiv, int fUseInv,
     Abc_Obj_t * pList;
     if ( stmm_count(tEquiv) == 0 )
         return;
-    // assign levels to the nodes of the network
-    Abc_NtkLevel( pNtk );
     // merge nodes in the classes
     if ( Abc_NtkHasMapping( pNtk ) )
     {
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index d4b15d59..a4c67a8b 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -313,6 +313,123 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
 
 /**Function*************************************************************
 
+  Synopsis    [Verifies sequential equivalence by fraiging followed by SAT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose )
+{
+    extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd );
+    extern Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nPartSizeLimit, int fVerbose );
+    extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
+    extern void * Abc_FrameGetGlobalFrame();
+
+    Vec_Vec_t * vParts;
+    Vec_Ptr_t * vOne;
+    Prove_Params_t Params, * pParams = &Params;
+    Abc_Ntk_t * pMiter, * pMiterPart;
+    int i, RetValue, Status, nOutputs;
+
+    // solve the CNF using the SAT solver
+    Prove_ParamsSetDefault( pParams );
+    pParams->nItersMax = 5;
+    //    pParams->fVerbose = 1;
+
+    // get the miter of the two networks
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 1 );
+    if ( pMiter == NULL )
+    {
+        printf( "Miter computation has failed.\n" );
+        return;
+    }
+    RetValue = Abc_NtkMiterIsConstant( pMiter );
+    if ( RetValue == 0 )
+    {
+        printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
+        // report the error
+        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
+        Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
+        FREE( pMiter->pModel );
+        Abc_NtkDelete( pMiter );
+        return;
+    }
+    if ( RetValue == 1 )
+    {
+        printf( "Networks are equivalent after structural hashing.\n" );
+        Abc_NtkDelete( pMiter );
+        return;
+    }
+
+    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
+
+    // partition the outputs
+    vParts = Abc_NtkPartitionSmart( pMiter, 50, 0 );
+
+    // fraig each partition
+    Status = 1;
+    nOutputs = 0;
+    Vec_VecForEachLevel( vParts, vOne, i )
+    {
+        // get this part of the miter
+        pMiterPart = Abc_NtkCreateConeArray( pMiter, vOne, 0 );
+        Abc_NtkCombinePos( pMiterPart, 0 );
+        // check the miter for being constant
+        RetValue = Abc_NtkMiterIsConstant( pMiterPart );
+        if ( RetValue == 0 )
+        {
+            printf( "Networks are NOT EQUIVALENT after partitioning.\n" );
+            Abc_NtkDelete( pMiterPart );
+            break;
+        }
+        if ( RetValue == 1 )
+        {
+            Abc_NtkDelete( pMiterPart );
+            continue;
+        }
+        // solve the problem
+        RetValue = Abc_NtkIvyProve( &pMiterPart, pParams );
+        if ( RetValue == -1 )
+        {
+            printf( "Networks are undecided (resource limits is reached).\r" );
+            Status = -1;
+        }
+        else if ( RetValue == 0 )
+        {
+            int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiterPart, pMiterPart->pModel );
+            if ( pSimInfo[0] != 1 )
+                printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
+            else
+                printf( "Networks are NOT EQUIVALENT.                 \n" );
+            free( pSimInfo );
+            Status = 0;
+            Abc_NtkDelete( pMiterPart );
+            break;
+        }
+        else
+        {
+            printf( "Finished part %d (out of %d)\r", i+1, Vec_VecSize(vParts) );
+            nOutputs += Vec_PtrSize(vOne);
+        }
+        Abc_NtkDelete( pMiterPart );
+    }
+    Vec_VecFree( vParts );
+
+    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
+
+    if ( Status == 1 )
+        printf( "Networks are equivalent.                         \n" );
+    else if ( Status == -1 )
+        printf( "Timed out after verifying %d outputs (out of %d).\n", nOutputs, Abc_NtkCoNum(pNtk1) );
+    Abc_NtkDelete( pMiter );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Verifies sequential equivalence by brute-force SAT.]
 
   Description []
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 5d5bccb8..9bc51dbe 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -7,6 +7,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcClpBdd.c \
     src/base/abci/abcClpSop.c \
     src/base/abci/abcCut.c \
+    src/base/abci/abcDar.c \
     src/base/abci/abcDebug.c \
     src/base/abci/abcDress.c \
     src/base/abci/abcDsd.c \
diff --git a/src/base/abci/xaaaa.c b/src/base/abci/xaaaa.c
new file mode 100644
index 00000000..ea39ad02
--- /dev/null
+++ b/src/base/abci/xaaaa.c
@@ -0,0 +1,155 @@
+/**CFile****************************************************************
+
+  FileName    [abc_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintMeasures( unsigned * pTruth, int nVars )
+{
+    unsigned uCofs[10][32];
+    int i, k, nOnes;
+
+    // total pairs
+    nOnes =  Kit_TruthCountOnes( uCofs[0], nVars );
+    printf( "Total = %d.\n", nOnes * ((1 << nVars) - nOnes) );
+
+    // print measures for individual variables
+    for ( i = 0; i < nVars; i++ )
+    {
+        Kit_TruthUniqueNew( uCofs[0], pTruth, nVars, i );
+        nOnes = Kit_TruthCountOnes( uCofs[0], nVars );
+        printf( "%7d ", nOnes );
+    }
+    printf( "\n" );
+
+    // consider pairs
+    for ( i = 0; i < nVars; i++ )
+    for ( k = 0; k < nVars; k++ )
+    {
+        if ( i == k )
+        {
+            printf( "        " );
+            continue;
+        }
+        Kit_TruthCofactor0New( uCofs[0], pTruth, nVars, i );
+        Kit_TruthCofactor1New( uCofs[1], pTruth, nVars, i );
+
+        Kit_TruthCofactor0New( uCofs[2], uCofs[0], nVars, k ); // 00
+        Kit_TruthCofactor1New( uCofs[3], uCofs[0], nVars, k ); // 01
+        Kit_TruthCofactor0New( uCofs[4], uCofs[1], nVars, k ); // 10
+        Kit_TruthCofactor1New( uCofs[5], uCofs[1], nVars, k ); // 11
+
+        Kit_TruthAndPhase( uCofs[6], uCofs[2], uCofs[5], nVars, 0, 1 ); // 00  & 11'
+        Kit_TruthAndPhase( uCofs[7], uCofs[2], uCofs[5], nVars, 1, 0 ); // 00' & 11
+        Kit_TruthAndPhase( uCofs[8], uCofs[3], uCofs[4], nVars, 0, 1 ); // 01  & 10'
+        Kit_TruthAndPhase( uCofs[9], uCofs[3], uCofs[4], nVars, 1, 0 ); // 01' & 10
+
+        nOnes = Kit_TruthCountOnes( uCofs[6], nVars ) + 
+                Kit_TruthCountOnes( uCofs[7], nVars ) + 
+                Kit_TruthCountOnes( uCofs[8], nVars ) + 
+                Kit_TruthCountOnes( uCofs[9], nVars );
+
+        printf( "%7d ", nOnes );
+        if ( k == nVars - 1 )
+            printf( "\n" );
+    }
+    printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_Ntk4VarTable( Abc_Ntk_t * pNtk )
+{
+    static u4VarTts[222] = {
+        0x0000, 0x0001, 0x0003, 0x0006, 0x0007, 0x000f, 0x0016, 0x0017, 0x0018, 0x0019, 
+        0x001b, 0x001e, 0x001f, 0x003c, 0x003d, 0x003f, 0x0069, 0x006b, 0x006f, 0x007e, 
+        0x007f, 0x00ff, 0x0116, 0x0117, 0x0118, 0x0119, 0x011a, 0x011b, 0x011e, 0x011f, 
+        0x012c, 0x012d, 0x012f, 0x013c, 0x013d, 0x013e, 0x013f, 0x0168, 0x0169, 0x016a, 
+        0x016b, 0x016e, 0x016f, 0x017e, 0x017f, 0x0180, 0x0181, 0x0182, 0x0183, 0x0186, 
+        0x0187, 0x0189, 0x018b, 0x018f, 0x0196, 0x0197, 0x0198, 0x0199, 0x019a, 0x019b, 
+        0x019e, 0x019f, 0x01a8, 0x01a9, 0x01aa, 0x01ab, 0x01ac, 0x01ad, 0x01ae, 0x01af, 
+        0x01bc, 0x01bd, 0x01be, 0x01bf, 0x01e8, 0x01e9, 0x01ea, 0x01eb, 0x01ee, 0x01ef, 
+        0x01fe, 0x033c, 0x033d, 0x033f, 0x0356, 0x0357, 0x0358, 0x0359, 0x035a, 0x035b, 
+        0x035e, 0x035f, 0x0368, 0x0369, 0x036a, 0x036b, 0x036c, 0x036d, 0x036e, 0x036f, 
+        0x037c, 0x037d, 0x037e, 0x03c0, 0x03c1, 0x03c3, 0x03c5, 0x03c6, 0x03c7, 0x03cf, 
+        0x03d4, 0x03d5, 0x03d6, 0x03d7, 0x03d8, 0x03d9, 0x03db, 0x03dc, 0x03dd, 0x03de, 
+        0x03fc, 0x0660, 0x0661, 0x0662, 0x0663, 0x0666, 0x0667, 0x0669, 0x066b, 0x066f, 
+        0x0672, 0x0673, 0x0676, 0x0678, 0x0679, 0x067a, 0x067b, 0x067e, 0x0690, 0x0691, 
+        0x0693, 0x0696, 0x0697, 0x069f, 0x06b0, 0x06b1, 0x06b2, 0x06b3, 0x06b4, 0x06b5, 
+        0x06b6, 0x06b7, 0x06b9, 0x06bd, 0x06f0, 0x06f1, 0x06f2, 0x06f6, 0x06f9, 0x0776, 
+        0x0778, 0x0779, 0x077a, 0x077e, 0x07b0, 0x07b1, 0x07b4, 0x07b5, 0x07b6, 0x07bc, 
+        0x07e0, 0x07e1, 0x07e2, 0x07e3, 0x07e6, 0x07e9, 0x07f0, 0x07f1, 0x07f2, 0x07f8, 
+        0x0ff0, 0x1668, 0x1669, 0x166a, 0x166b, 0x166e, 0x167e, 0x1681, 0x1683, 0x1686, 
+        0x1687, 0x1689, 0x168b, 0x168e, 0x1696, 0x1697, 0x1698, 0x1699, 0x169a, 0x169b, 
+        0x169e, 0x16a9, 0x16ac, 0x16ad, 0x16bc, 0x16e9, 0x177e, 0x178e, 0x1796, 0x1798, 
+        0x179a, 0x17ac, 0x17e8, 0x18e7, 0x19e1, 0x19e3, 0x19e6, 0x1bd8, 0x1be4, 0x1ee1, 
+        0x3cc3, 0x6996
+    };
+    int Counters[222];
+
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj;
+    int i;
+
+    // set elementary truth tables
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        pObj
+
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        vNodes = Abc_NtkDfsNodes( pNtk, &pObj, i );
+        Vec_PtrFree( vNodes );
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index 48738903..a54a00fe 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -25,7 +25,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static unsigned Io_ReadAigerDecode( char ** ppPos );
+unsigned Io_ReadAigerDecode( char ** ppPos );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index a1ff4456..7c9da184 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -129,7 +129,7 @@ static unsigned Io_ObjMakeLit( int Var, int fCompl )                 { return (V
 static unsigned Io_ObjAigerNum( Abc_Obj_t * pObj )                   { return (unsigned)pObj->pCopy;  }
 static void     Io_ObjSetAigerNum( Abc_Obj_t * pObj, unsigned Num )  { pObj->pCopy = (void *)Num;     }
 
-static int      Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
+int      Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c
index bf5182fb..a02d53fd 100644
--- a/src/base/io/ioWriteVerilog.c
+++ b/src/base/io/ioWriteVerilog.c
@@ -213,17 +213,33 @@ void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
 ***********************************************************************/
 void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
 {
-    Abc_Obj_t * pTerm, * pNet;
+    Abc_Obj_t * pTerm, * pNet, * pSkip;
     int LineLength;
     int AddedLength;
     int NameCounter;
     int i;
+    int nskip;
+
+    pSkip = 0;
+    nskip = 0;
 
     LineLength  = Start;
     NameCounter = 0;
     Abc_NtkForEachPo( pNtk, pTerm, i )
     {
         pNet = Abc_ObjFanin0(pTerm);
+        
+        if ( Abc_ObjIsPi(Abc_ObjFanin0(pNet)) )
+        {
+            // Skip this output since it is a feedthrough -- the same
+            // name will appear as an input and an output which other
+            // tools reading verilog do not like.
+            
+            nskip++;
+            pSkip = pNet;   // save an example of skipped net
+            continue;
+        }
+        
         // get the line length after this name is written
         AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
         if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
@@ -237,6 +253,14 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
         LineLength += AddedLength;
         NameCounter++;
     }
+
+    if (nskip != 0)
+    {
+        assert (pSkip);
+        printf( "Io_WriteVerilogPos(): Omitted %d feedthrough nets from output list of module (e.g. %s).\n", nskip, Abc_ObjName(pSkip) );
+        return;
+    }
+
 }
 
 /**Function*************************************************************
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 13c71759..8c316970 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#ifndef __Abc_INT_H__
-#define __Abc_INT_H__
+#ifndef __MAIN_INT_H__
+#define __MAIN_INT_H__
 
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///