Version abc50904

35 files changed, 966 insertions, 983 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 81a1c328..bff4f9f1 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -165,6 +165,8 @@ struct Abc_Ntk_t_
     // level information (for AIGs)
     int              LevelMax;      // maximum number of levels
     Vec_Int_t *      vLevelsR;      // level in the reverse topological order 
+    // support information
+    Vec_Ptr_t *      vSupps;
     // the external don't-care if given
     Abc_Ntk_t *      pExdc;         // the EXDC network
     // miscellaneous data members
@@ -415,39 +417,6 @@ extern bool               Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
 extern bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 /*=== abcCollapse.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose );
-/*=== abcCreate.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func );
-extern Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
-extern void               Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
-extern void               Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkStartRead( char * pName );
-extern void               Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkDup( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis );
-extern Abc_Ntk_t *        Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues );
-extern Abc_Ntk_t *        Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode );
-extern void               Abc_NtkDelete( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
-extern Abc_Obj_t *        Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew );
-extern Abc_Obj_t *        Abc_NtkDupReset( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew );
-extern void               Abc_NtkDeleteObj( Abc_Obj_t * pObj );
-extern Abc_Obj_t *        Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t *        Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t *        Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t *        Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t *        Abc_NtkCreateNode( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NtkCreatePi( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NtkCreatePo( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NtkCreateLatch( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NodeCreateConst0( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NodeCreateConst1( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NodeCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
-extern Abc_Obj_t *        Abc_NodeCreateBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
-extern Abc_Obj_t *        Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
-extern Abc_Obj_t *        Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
-extern Abc_Obj_t *        Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 );
-extern Abc_Obj_t *        Abc_NodeClone( Abc_Obj_t * pNode );
 /*=== abcCut.c ==========================================================*/
 extern void *             Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj );
 extern void *             Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj );
@@ -486,7 +455,6 @@ extern void               Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch );
 extern int                Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk );
 /*=== abcMap.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fVerbose );
 extern int                Abc_NtkUnmap( Abc_Ntk_t * pNtk );
 /*=== abcMiter.c ==========================================================*/
 extern int                Abc_NtkMinimumBase( Abc_Ntk_t * pNtk );
@@ -495,11 +463,35 @@ extern int                Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk );
 extern int                Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
 /*=== abcMiter.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
-extern Abc_Ntk_t *        Abc_NtkMiterOne( Abc_Ntk_t * pNtk, int Out, int In1, int In2 );
+extern Abc_Ntk_t *        Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 );
 extern int                Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter );
 extern void               Abc_NtkMiterReport( Abc_Ntk_t * pMiter );
 extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
 extern Abc_Ntk_t *        Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial );
+/*=== abcObj.c ==========================================================*/
+extern Abc_Obj_t *        Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
+extern void               Abc_ObjRecycle( Abc_Obj_t * pObj );
+extern void               Abc_ObjAdd( Abc_Obj_t * pObj );
+extern Abc_Obj_t *        Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
+extern Abc_Obj_t *        Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew );
+extern Abc_Obj_t *        Abc_NtkDupReset( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew );
+extern void               Abc_NtkDeleteObj( Abc_Obj_t * pObj );
+extern Abc_Obj_t *        Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
+extern Abc_Obj_t *        Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
+extern Abc_Obj_t *        Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
+extern Abc_Obj_t *        Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName );
+extern Abc_Obj_t *        Abc_NtkCreateNode( Abc_Ntk_t * pNtk );
+extern Abc_Obj_t *        Abc_NtkCreatePi( Abc_Ntk_t * pNtk );
+extern Abc_Obj_t *        Abc_NtkCreatePo( Abc_Ntk_t * pNtk );
+extern Abc_Obj_t *        Abc_NtkCreateLatch( Abc_Ntk_t * pNtk );
+extern Abc_Obj_t *        Abc_NodeCreateConst0( Abc_Ntk_t * pNtk );
+extern Abc_Obj_t *        Abc_NodeCreateConst1( Abc_Ntk_t * pNtk );
+extern Abc_Obj_t *        Abc_NodeCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
+extern Abc_Obj_t *        Abc_NodeCreateBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
+extern Abc_Obj_t *        Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
+extern Abc_Obj_t *        Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
+extern Abc_Obj_t *        Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 );
+extern Abc_Obj_t *        Abc_NodeClone( Abc_Obj_t * pNode );
 /*=== abcNames.c ====================================================*/
 extern char *             Abc_NtkRegisterName( Abc_Ntk_t * pNtk, char * pName );
 extern char *             Abc_NtkRegisterNamePlus( Abc_Ntk_t * pNtk, char * pName, char * pSuffix );
@@ -529,6 +521,20 @@ extern Abc_Ntk_t *        Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc,
 extern Abc_Ntk_t *        Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk );
 extern DdManager *        Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly );
 extern void               Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk );
+/*=== abcNtk.c ==========================================================*/
+extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func );
+extern Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
+extern void               Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+extern void               Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+extern void               Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t *        Abc_NtkStartRead( char * pName );
+extern void               Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t *        Abc_NtkDup( Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t *        Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis );
+extern Abc_Ntk_t *        Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues );
+extern Abc_Ntk_t *        Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode );
+extern void               Abc_NtkDelete( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk );
 /*=== abcPrint.c ==========================================================*/
 extern void               Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored );
 extern void               Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
new file mode 100644
index 00000000..5c199141
--- /dev/null
+++ b/src/base/abc/abcNtk.c
@@ -0,0 +1,592 @@
+/**CFile****************************************************************
+
+  FileName    [abcNtk.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Network creation/duplication/deletion procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcNtk.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "main.h"
+#include "mio.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define ABC_NUM_STEPS  10
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new Ntk.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
+{
+    Abc_Ntk_t * pNtk;
+    pNtk = ALLOC( Abc_Ntk_t, 1 );
+    memset( pNtk, 0, sizeof(Abc_Ntk_t) );
+    pNtk->ntkType     = Type;
+    pNtk->ntkFunc     = Func;
+    // start the object storage
+    pNtk->vObjs       = Vec_PtrAlloc( 100 );
+    pNtk->vLats       = Vec_PtrAlloc( 100 );
+    pNtk->vCis        = Vec_PtrAlloc( 100 );
+    pNtk->vCos        = Vec_PtrAlloc( 100 );
+    pNtk->vPtrTemp    = Vec_PtrAlloc( 100 );
+    pNtk->vIntTemp    = Vec_IntAlloc( 100 );
+    pNtk->vStrTemp    = Vec_StrAlloc( 100 );
+    // start the hash table
+    pNtk->tName2Net   = stmm_init_table(strcmp, stmm_strhash);
+    pNtk->tObj2Name   = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
+    // start the memory managers
+    pNtk->pMmNames    = Extra_MmFlexStart();
+    pNtk->pMmObj      = Extra_MmFixedStart( sizeof(Abc_Obj_t) );
+    pNtk->pMmStep     = Extra_MmStepStart( ABC_NUM_STEPS );
+    // get ready to assign the first Obj ID
+    pNtk->nTravIds    = 1;
+    // start the functionality manager
+    if ( Abc_NtkHasSop(pNtk) )
+        pNtk->pManFunc = Extra_MmFlexStart();
+    else if ( Abc_NtkHasBdd(pNtk) )
+        pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    else if ( Abc_NtkHasAig(pNtk) )
+        pNtk->pManFunc = Abc_AigAlloc( pNtk );
+    else if ( Abc_NtkHasMapping(pNtk) )
+        pNtk->pManFunc = Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame());
+    else
+        assert( 0 );
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts a new network using existing network as a model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func )
+{
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pObjNew;
+    int i;
+    if ( pNtk == NULL )
+        return NULL;
+    // start the network
+    pNtkNew = Abc_NtkAlloc( Type, Func );
+    // duplicate the name and the spec
+    pNtkNew->pName = util_strsav(pNtk->pName);
+    pNtkNew->pSpec = util_strsav(pNtk->pSpec);
+    // clone the PIs/POs/latches
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        pObjNew = Abc_NtkDupObj(pNtkNew, pObj);
+        Vec_PtrPush( pNtkNew->vCis, pObjNew );
+        Vec_PtrPush( pNtkNew->vCos, pObjNew );
+    }
+    // clean the node copy fields
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        pObj->pCopy = NULL;
+    // transfer the names
+    Abc_NtkDupCioNamesTable( pNtk, pNtkNew );
+    Abc_ManTimeDup( pNtk, pNtkNew );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finalizes the network using the existing network as a model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
+{
+    Abc_Obj_t * pObj, * pDriver, * pDriverNew;
+    int i;
+    // set the COs of the strashed network
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        pDriver    = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pObj) );
+        pDriverNew = Abc_ObjNotCond(pDriver->pCopy, Abc_ObjFaninC0(pObj));
+        Abc_ObjAddFanin( pObj->pCopy, pDriverNew );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finalizes the network using the existing network as a model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
+{
+    Abc_Obj_t * pObj, * pDriver, * pDriverNew;
+    int i;
+    // set the COs of the strashed network
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        pDriver    = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pObj) );
+        pDriverNew = pDriver->pCopy;
+        Abc_ObjAddFanin( pObj->pCopy, pDriverNew );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finalizes the network adding latches to CI/CO lists and creates their names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pLatch;
+    int i;
+    // set the COs of the strashed network
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        Vec_PtrPush( pNtk->vCis, pLatch );
+        Vec_PtrPush( pNtk->vCos, pLatch );
+        Abc_NtkLogicStoreName( pLatch, Abc_ObjNameSuffix(pLatch, "L") );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts a new network using existing network as a model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkStartRead( char * pName )
+{
+    Abc_Ntk_t * pNtkNew; 
+    // allocate the empty network
+    pNtkNew = Abc_NtkAlloc( ABC_TYPE_NETLIST, ABC_FUNC_SOP );
+    // set the specs
+    pNtkNew->pName = util_strsav( pName );
+    pNtkNew->pSpec = util_strsav( pName );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finalizes the network using the existing network as a model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pLatch;
+    int i;
+    assert( Abc_NtkIsNetlist(pNtk) );
+    // fix the net drivers
+    Abc_NtkFixNonDrivenNets( pNtk );
+    // create the names table
+    Abc_NtkCreateCioNamesTable( pNtk );
+    // add latches to the CI/CO arrays
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        Vec_PtrPush( pNtk->vCis, pLatch );
+        Vec_PtrPush( pNtk->vCos, pLatch );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicate the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k;
+    if ( pNtk == NULL )
+        return NULL;
+    // start the network
+    pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc );
+    // copy the internal nodes
+    if ( Abc_NtkHasAig(pNtk) )
+        Abc_AigDup( pNtk->pManFunc, pNtkNew->pManFunc );
+    else
+    {
+        // duplicate the nets and nodes (CIs/COs/latches already dupped)
+        Abc_NtkForEachObj( pNtk, pObj, i )
+            if ( pObj->pCopy == NULL )
+                Abc_NtkDupObj(pNtkNew, pObj);
+        // reconnect all objects (no need to transfer attributes on edges)
+        Abc_NtkForEachObj( pNtk, pObj, i )
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+    }
+    // duplicate the EXDC Ntk
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkDup(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the network composed of one output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pFanin;
+    char Buffer[1000];
+    int i, k;
+
+    assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) );
+    assert( Abc_ObjIsCo(pNode) ); 
+    
+    // start the network
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    // set the name
+    sprintf( Buffer, "%s_%s", pNtk->pName, Abc_ObjName(pNode) );
+    pNtkNew->pName = util_strsav(Buffer);
+
+    // collect the nodes in the TFI of the output
+    vNodes = Abc_NtkDfsNodes( pNtk, &pNode, 1 );
+    // create the PIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+    {
+        if ( fUseAllCis || Abc_NodeIsTravIdCurrent(pObj) ) // TravId is set by DFS
+        {
+            pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
+            Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
+        }
+    }
+    // establish connection between the constant nodes
+    if ( Abc_NtkIsStrash(pNtk) )
+        Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc);
+
+    // copy the nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // if it is an AIG, add to the hash table
+        if ( Abc_NtkIsStrash(pNtk) )
+        {
+            pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+        }
+        else
+        {
+            Abc_NtkDupObj( pNtkNew, pObj );
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+        }
+    }
+    Vec_PtrFree( vNodes );
+
+    // add the PO corresponding to this output
+    pNode->pCopy = Abc_NtkCreatePo( pNtkNew );
+    Abc_ObjAddFanin( pNode->pCopy, Abc_ObjFanin0(pNode)->pCopy );
+    Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) );
+
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkSplitOutput(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the network composed of one output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pFinal, * pOther, * pNodePo;
+    int i;
+
+    assert( Abc_NtkIsLogic(pNtk) );
+    
+    // start the network
+    Abc_NtkCleanCopy( pNtk );
+    pNtkNew = Abc_NtkAlloc( ABC_TYPE_STRASH, ABC_FUNC_AIG );
+    pNtkNew->pName = util_strsav(pNtk->pName);
+
+    // collect the nodes in the TFI of the output
+    vNodes = Abc_NtkDfsNodes( pNtk, (Abc_Obj_t **)vRoots->pArray, vRoots->nSize );
+    // create the PIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+    {
+        pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
+    }
+    // copy the nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = Abc_NodeStrash( pNtkNew->pManFunc, pObj );
+    Vec_PtrFree( vNodes );
+
+    // add the PO
+    pFinal = Abc_AigConst1( pNtkNew->pManFunc );
+    Vec_PtrForEachEntry( vRoots, pObj, i )
+    {
+        pOther = pObj->pCopy;
+        if ( Vec_IntEntry(vValues, i) == 0 )
+            pOther = Abc_ObjNot(pOther);
+        pFinal = Abc_AigAnd( pNtkNew->pManFunc, pFinal, pOther );
+    }
+
+    // add the PO corresponding to this output
+    pNodePo = Abc_NtkCreatePo( pNtkNew );
+    Abc_ObjAddFanin( pNodePo, pFinal );
+    Abc_NtkLogicStoreName( pNodePo, "miter" );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the Ntk.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
+{    
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pFanin, * pNodePo;
+    int i;
+    // start the network
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    pNtkNew->pName = util_strsav(Abc_ObjName(pNode));
+    // add the PIs corresponding to the fanins of the node
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+    {
+        pFanin->pCopy = Abc_NtkCreatePi( pNtkNew );
+        Abc_NtkLogicStoreName( pFanin->pCopy, Abc_ObjName(pFanin) );
+    }
+    // duplicate and connect the node
+    pNode->pCopy = Abc_NtkDupObj( pNtkNew, pNode );
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        Abc_ObjAddFanin( pNode->pCopy, pFanin->pCopy );
+    // create the only PO
+    pNodePo = Abc_NtkCreatePo( pNtkNew );
+    Abc_ObjAddFanin( pNodePo, pNode->pCopy );
+    Abc_NtkLogicStoreName( pNodePo, Abc_ObjName(pNode) );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkSplitNode(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the Ntk.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDelete( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int TotalMemory, i;
+    int LargePiece = (4 << ABC_NUM_STEPS);
+    if ( pNtk == NULL )
+        return;
+    // make sure all the marks are clean
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        // free large fanout arrays
+        if ( pObj->vFanouts.nCap * 4 > LargePiece )
+            FREE( pObj->vFanouts.pArray );
+        // check that the other things are okay
+        assert( pObj->fMarkA == 0 );
+        assert( pObj->fMarkB == 0 );
+        assert( pObj->fMarkC == 0 );
+    }
+
+    // dereference the BDDs
+    if ( Abc_NtkHasBdd(pNtk) )
+        Abc_NtkForEachNode( pNtk, pObj, i )
+            Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData );
+        
+    FREE( pNtk->pName );
+    FREE( pNtk->pSpec );
+    // copy the EXDC Ntk
+    if ( pNtk->pExdc )
+        Abc_NtkDelete( pNtk->pExdc );
+    // free the arrays
+    Vec_PtrFree( pNtk->vObjs );
+    Vec_PtrFree( pNtk->vLats );
+    Vec_PtrFree( pNtk->vCis );
+    Vec_PtrFree( pNtk->vCos );
+    Vec_PtrFree( pNtk->vPtrTemp );
+    Vec_IntFree( pNtk->vIntTemp );
+    Vec_StrFree( pNtk->vStrTemp );
+    // free the hash table of Obj name into Obj ID
+    stmm_free_table( pNtk->tName2Net );
+    stmm_free_table( pNtk->tObj2Name );
+    TotalMemory  = 0;
+    TotalMemory += Extra_MmFlexReadMemUsage(pNtk->pMmNames);
+    TotalMemory += Extra_MmFixedReadMemUsage(pNtk->pMmObj);
+    TotalMemory += Extra_MmStepReadMemUsage(pNtk->pMmStep);
+//    fprintf( stdout, "The total memory allocated internally by the network = %0.2f Mb.\n", ((double)TotalMemory)/(1<<20) );
+    // free the storage 
+    Extra_MmFlexStop ( pNtk->pMmNames, 0 );
+    Extra_MmFixedStop( pNtk->pMmObj,   0 );
+    Extra_MmStepStop ( pNtk->pMmStep,  0 );
+    // free the timing manager
+    if ( pNtk->pManTime )
+        Abc_ManTimeStop( pNtk->pManTime );
+    // start the functionality manager
+    if ( Abc_NtkHasSop(pNtk) )
+        Extra_MmFlexStop( pNtk->pManFunc, 0 );
+    else if ( Abc_NtkHasBdd(pNtk) )
+        Extra_StopManager( pNtk->pManFunc );
+    else if ( Abc_NtkHasAig(pNtk) )
+        Abc_AigFree( pNtk->pManFunc );
+    else if ( !Abc_NtkHasMapping(pNtk) )
+        assert( 0 );
+    free( pNtk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the verilog file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk )
+{ 
+    Vec_Ptr_t * vNets;
+    Abc_Obj_t * pNet, * pNode;
+    int i;
+
+    // check for non-driven nets
+    vNets = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachNet( pNtk, pNet, i )
+    {
+        if ( Abc_ObjFaninNum(pNet) > 0 )
+            continue;
+        // add the constant 0 driver
+        pNode = Abc_NtkCreateNode( pNtk );
+        // set the constant function
+        Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, " 0\n") );
+        // add the fanout net
+        Abc_ObjAddFanin( pNet, pNode );
+        // add the net to those for which the warning will be printed
+        Vec_PtrPush( vNets, pNet->pData );
+    }
+
+    // print the warning
+    if ( vNets->nSize > 0 )
+    {
+        printf( "Constant-zero drivers were added to %d non-driven nets:\n", vNets->nSize );
+        for ( i = 0; i < vNets->nSize; i++ )
+        {
+            if ( i == 0 )
+                printf( "%s", vNets->pArray[i] );
+            else if ( i == 1 )
+                printf( ", %s", vNets->pArray[i] );
+            else if ( i == 2 )
+            {
+                printf( ", %s, etc.", vNets->pArray[i] );
+                break;
+            }
+        }
+        printf( "\n" );
+    }
+    Vec_PtrFree( vNets );
+}
+
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abc/abcCreate.c b/src/base/abc/abcObj.c
index 16d5ec05..f869abf3 100644
--- a/src/base/abc/abcCreate.c
+++ b/src/base/abc/abcObj.c
@@ -6,7 +6,7 @@
 
   PackageName [Network and node package.]
 
-  Synopsis    [Creation/duplication/deletion procedures.]
+  Synopsis    [Object creation/duplication/deletion procedures.]
 
   Author      [Alan Mishchenko]
   
@@ -26,547 +26,12 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define ABC_NUM_STEPS  10
-
-static Abc_Obj_t *   Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
-static void          Abc_ObjRecycle( Abc_Obj_t * pObj );
-static void          Abc_ObjAdd( Abc_Obj_t * pObj );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Creates a new Ntk.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
-{
-    Abc_Ntk_t * pNtk;
-    pNtk = ALLOC( Abc_Ntk_t, 1 );
-    memset( pNtk, 0, sizeof(Abc_Ntk_t) );
-    pNtk->ntkType     = Type;
-    pNtk->ntkFunc     = Func;
-    // start the object storage
-    pNtk->vObjs       = Vec_PtrAlloc( 100 );
-    pNtk->vLats       = Vec_PtrAlloc( 100 );
-    pNtk->vCis        = Vec_PtrAlloc( 100 );
-    pNtk->vCos        = Vec_PtrAlloc( 100 );
-    pNtk->vPtrTemp    = Vec_PtrAlloc( 100 );
-    pNtk->vIntTemp    = Vec_IntAlloc( 100 );
-    pNtk->vStrTemp    = Vec_StrAlloc( 100 );
-    // start the hash table
-    pNtk->tName2Net   = stmm_init_table(strcmp, stmm_strhash);
-    pNtk->tObj2Name   = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
-    // start the memory managers
-    pNtk->pMmNames    = Extra_MmFlexStart();
-    pNtk->pMmObj      = Extra_MmFixedStart( sizeof(Abc_Obj_t) );
-    pNtk->pMmStep     = Extra_MmStepStart( ABC_NUM_STEPS );
-    // get ready to assign the first Obj ID
-    pNtk->nTravIds    = 1;
-    // start the functionality manager
-    if ( Abc_NtkHasSop(pNtk) )
-        pNtk->pManFunc = Extra_MmFlexStart();
-    else if ( Abc_NtkHasBdd(pNtk) )
-        pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    else if ( Abc_NtkHasAig(pNtk) )
-        pNtk->pManFunc = Abc_AigAlloc( pNtk );
-    else if ( Abc_NtkHasMapping(pNtk) )
-        pNtk->pManFunc = Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame());
-    else
-        assert( 0 );
-    return pNtk;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Starts a new network using existing network as a model.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func )
-{
-    Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObj, * pObjNew;
-    int i;
-    if ( pNtk == NULL )
-        return NULL;
-    // start the network
-    pNtkNew = Abc_NtkAlloc( Type, Func );
-    // duplicate the name and the spec
-    pNtkNew->pName = util_strsav(pNtk->pName);
-    pNtkNew->pSpec = util_strsav(pNtk->pSpec);
-    // clone the PIs/POs/latches
-    Abc_NtkForEachPi( pNtk, pObj, i )
-        Abc_NtkDupObj(pNtkNew, pObj);
-    Abc_NtkForEachPo( pNtk, pObj, i )
-        Abc_NtkDupObj(pNtkNew, pObj);
-    Abc_NtkForEachLatch( pNtk, pObj, i )
-    {
-        pObjNew = Abc_NtkDupObj(pNtkNew, pObj);
-        Vec_PtrPush( pNtkNew->vCis, pObjNew );
-        Vec_PtrPush( pNtkNew->vCos, pObjNew );
-    }
-    // clean the node copy fields
-    Abc_NtkForEachNode( pNtk, pObj, i )
-        pObj->pCopy = NULL;
-    // transfer the names
-    Abc_NtkDupCioNamesTable( pNtk, pNtkNew );
-    Abc_ManTimeDup( pNtk, pNtkNew );
-    return pNtkNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Finalizes the network using the existing network as a model.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
-{
-    Abc_Obj_t * pObj, * pDriver, * pDriverNew;
-    int i;
-    // set the COs of the strashed network
-    Abc_NtkForEachCo( pNtk, pObj, i )
-    {
-        pDriver    = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pObj) );
-        pDriverNew = Abc_ObjNotCond(pDriver->pCopy, Abc_ObjFaninC0(pObj));
-        Abc_ObjAddFanin( pObj->pCopy, pDriverNew );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Finalizes the network adding latches to CI/CO lists and creates their names.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pLatch;
-    int i;
-    // set the COs of the strashed network
-    Abc_NtkForEachLatch( pNtk, pLatch, i )
-    {
-        Vec_PtrPush( pNtk->vCis, pLatch );
-        Vec_PtrPush( pNtk->vCos, pLatch );
-        Abc_NtkLogicStoreName( pLatch, Abc_ObjNameSuffix(pLatch, "L") );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Starts a new network using existing network as a model.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkStartRead( char * pName )
-{
-    Abc_Ntk_t * pNtkNew; 
-    // allocate the empty network
-    pNtkNew = Abc_NtkAlloc( ABC_TYPE_NETLIST, ABC_FUNC_SOP );
-    // set the specs
-    pNtkNew->pName = util_strsav( pName );
-    pNtkNew->pSpec = util_strsav( pName );
-    return pNtkNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Finalizes the network using the existing network as a model.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pLatch;
-    int i;
-    assert( Abc_NtkIsNetlist(pNtk) );
-    // fix the net drivers
-    Abc_NtkFixNonDrivenNets( pNtk );
-    // create the names table
-    Abc_NtkCreateCioNamesTable( pNtk );
-    // add latches to the CI/CO arrays
-    Abc_NtkForEachLatch( pNtk, pLatch, i )
-    {
-        Vec_PtrPush( pNtk->vCis, pLatch );
-        Vec_PtrPush( pNtk->vCos, pLatch );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicate the network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
-{
-    Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObj, * pFanin;
-    int i, k;
-    if ( pNtk == NULL )
-        return NULL;
-    // start the network
-    pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc );
-    // copy the internal nodes
-    if ( Abc_NtkHasAig(pNtk) )
-        Abc_AigDup( pNtk->pManFunc, pNtkNew->pManFunc );
-    else
-    {
-        // duplicate the nets and nodes (CIs/COs/latches already dupped)
-        Abc_NtkForEachObj( pNtk, pObj, i )
-            if ( pObj->pCopy == NULL )
-                Abc_NtkDupObj(pNtkNew, pObj);
-        // reconnect all objects (no need to transfer attributes on edges)
-        Abc_NtkForEachObj( pNtk, pObj, i )
-            Abc_ObjForEachFanin( pObj, pFanin, k )
-                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
-    }
-    // duplicate the EXDC Ntk
-    if ( pNtk->pExdc )
-        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
-    if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkDup(): Network check has failed.\n" );
-    return pNtkNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the network composed of one output.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis )
-{
-    Vec_Ptr_t * vNodes;
-    Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObj, * pFanin;
-    char Buffer[1000];
-    int i, k;
-
-    assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) );
-    assert( Abc_ObjIsCo(pNode) ); 
-    
-    // start the network
-    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
-    // set the name
-    sprintf( Buffer, "%s_%s", pNtk->pName, Abc_ObjName(pNode) );
-    pNtkNew->pName = util_strsav(Buffer);
-
-    // collect the nodes in the TFI of the output
-    vNodes = Abc_NtkDfsNodes( pNtk, &pNode, 1 );
-    // create the PIs
-    Abc_NtkForEachCi( pNtk, pObj, i )
-    {
-        if ( fUseAllCis || Abc_NodeIsTravIdCurrent(pObj) ) // TravId is set by DFS
-        {
-            pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
-            Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
-        }
-    }
-    // establish connection between the constant nodes
-    if ( Abc_NtkIsStrash(pNtk) )
-        Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc);
-
-    // copy the nodes
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-    {
-        // if it is an AIG, add to the hash table
-        if ( Abc_NtkIsStrash(pNtk) )
-        {
-            pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
-        }
-        else
-        {
-            Abc_NtkDupObj( pNtkNew, pObj );
-            Abc_ObjForEachFanin( pObj, pFanin, k )
-                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
-        }
-    }
-    Vec_PtrFree( vNodes );
-
-    // add the PO corresponding to this output
-    pNode->pCopy = Abc_NtkCreatePo( pNtkNew );
-    Abc_ObjAddFanin( pNode->pCopy, Abc_ObjFanin0(pNode)->pCopy );
-    Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) );
-
-    if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkSplitOutput(): Network check has failed.\n" );
-    return pNtkNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the network composed of one output.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues )
-{
-    Vec_Ptr_t * vNodes;
-    Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObj, * pFinal, * pOther, * pNodePo;
-    int i;
-
-    assert( Abc_NtkIsLogic(pNtk) );
-    
-    // start the network
-    Abc_NtkCleanCopy( pNtk );
-    pNtkNew = Abc_NtkAlloc( ABC_TYPE_STRASH, ABC_FUNC_AIG );
-    pNtkNew->pName = util_strsav(pNtk->pName);
-
-    // collect the nodes in the TFI of the output
-    vNodes = Abc_NtkDfsNodes( pNtk, (Abc_Obj_t **)vRoots->pArray, vRoots->nSize );
-    // create the PIs
-    Abc_NtkForEachCi( pNtk, pObj, i )
-    {
-        pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
-        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
-    }
-    // copy the nodes
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->pCopy = Abc_NodeStrash( pNtkNew->pManFunc, pObj );
-    Vec_PtrFree( vNodes );
-
-    // add the PO
-    pFinal = Abc_AigConst1( pNtkNew->pManFunc );
-    Vec_PtrForEachEntry( vRoots, pObj, i )
-    {
-        pOther = pObj->pCopy;
-        if ( Vec_IntEntry(vValues, i) == 0 )
-            pOther = Abc_ObjNot(pOther);
-        pFinal = Abc_AigAnd( pNtkNew->pManFunc, pFinal, pOther );
-    }
-
-    // add the PO corresponding to this output
-    pNodePo = Abc_NtkCreatePo( pNtkNew );
-    Abc_ObjAddFanin( pNodePo, pFinal );
-    Abc_NtkLogicStoreName( pNodePo, "miter" );
-    if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
-    return pNtkNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deletes the Ntk.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
-{    
-    Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pFanin, * pNodePo;
-    int i;
-    // start the network
-    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
-    pNtkNew->pName = util_strsav(Abc_ObjName(pNode));
-    // add the PIs corresponding to the fanins of the node
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-    {
-        pFanin->pCopy = Abc_NtkCreatePi( pNtkNew );
-        Abc_NtkLogicStoreName( pFanin->pCopy, Abc_ObjName(pFanin) );
-    }
-    // duplicate and connect the node
-    pNode->pCopy = Abc_NtkDupObj( pNtkNew, pNode );
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-        Abc_ObjAddFanin( pNode->pCopy, pFanin->pCopy );
-    // create the only PO
-    pNodePo = Abc_NtkCreatePo( pNtkNew );
-    Abc_ObjAddFanin( pNodePo, pNode->pCopy );
-    Abc_NtkLogicStoreName( pNodePo, Abc_ObjName(pNode) );
-    if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkSplitNode(): Network check has failed.\n" );
-    return pNtkNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deletes the Ntk.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkDelete( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pObj;
-    int TotalMemory, i;
-    int LargePiece = (4 << ABC_NUM_STEPS);
-    if ( pNtk == NULL )
-        return;
-    // make sure all the marks are clean
-    Abc_NtkForEachObj( pNtk, pObj, i )
-    {
-        // free large fanout arrays
-        if ( pObj->vFanouts.nCap * 4 > LargePiece )
-            FREE( pObj->vFanouts.pArray );
-        // check that the other things are okay
-        assert( pObj->fMarkA == 0 );
-        assert( pObj->fMarkB == 0 );
-        assert( pObj->fMarkC == 0 );
-    }
-
-    // dereference the BDDs
-    if ( Abc_NtkHasBdd(pNtk) )
-        Abc_NtkForEachNode( pNtk, pObj, i )
-            Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData );
-        
-    FREE( pNtk->pName );
-    FREE( pNtk->pSpec );
-    // copy the EXDC Ntk
-    if ( pNtk->pExdc )
-        Abc_NtkDelete( pNtk->pExdc );
-    // free the arrays
-    Vec_PtrFree( pNtk->vObjs );
-    Vec_PtrFree( pNtk->vLats );
-    Vec_PtrFree( pNtk->vCis );
-    Vec_PtrFree( pNtk->vCos );
-    Vec_PtrFree( pNtk->vPtrTemp );
-    Vec_IntFree( pNtk->vIntTemp );
-    Vec_StrFree( pNtk->vStrTemp );
-    // free the hash table of Obj name into Obj ID
-    stmm_free_table( pNtk->tName2Net );
-    stmm_free_table( pNtk->tObj2Name );
-    TotalMemory  = 0;
-    TotalMemory += Extra_MmFlexReadMemUsage(pNtk->pMmNames);
-    TotalMemory += Extra_MmFixedReadMemUsage(pNtk->pMmObj);
-    TotalMemory += Extra_MmStepReadMemUsage(pNtk->pMmStep);
-//    fprintf( stdout, "The total memory allocated internally by the network = %0.2f Mb.\n", ((double)TotalMemory)/(1<<20) );
-    // free the storage 
-    Extra_MmFlexStop ( pNtk->pMmNames, 0 );
-    Extra_MmFixedStop( pNtk->pMmObj,   0 );
-    Extra_MmStepStop ( pNtk->pMmStep,  0 );
-    // free the timing manager
-    if ( pNtk->pManTime )
-        Abc_ManTimeStop( pNtk->pManTime );
-    // start the functionality manager
-    if ( Abc_NtkHasSop(pNtk) )
-        Extra_MmFlexStop( pNtk->pManFunc, 0 );
-    else if ( Abc_NtkHasBdd(pNtk) )
-        Extra_StopManager( pNtk->pManFunc );
-    else if ( Abc_NtkHasAig(pNtk) )
-        Abc_AigFree( pNtk->pManFunc );
-    else if ( !Abc_NtkHasMapping(pNtk) )
-        assert( 0 );
-    free( pNtk );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reads the verilog file.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk )
-{ 
-    Vec_Ptr_t * vNets;
-    Abc_Obj_t * pNet, * pNode;
-    int i;
-
-    // check for non-driven nets
-    vNets = Vec_PtrAlloc( 100 );
-    Abc_NtkForEachNet( pNtk, pNet, i )
-    {
-        if ( Abc_ObjFaninNum(pNet) > 0 )
-            continue;
-        // add the constant 0 driver
-        pNode = Abc_NtkCreateNode( pNtk );
-        // set the constant function
-        Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, " 0\n") );
-        // add the fanout net
-        Abc_ObjAddFanin( pNet, pNode );
-        // add the net to those for which the warning will be printed
-        Vec_PtrPush( vNets, pNet->pData );
-    }
-
-    // print the warning
-    if ( vNets->nSize > 0 )
-    {
-        printf( "Constant-zero drivers were added to %d non-driven nets:\n", vNets->nSize );
-        for ( i = 0; i < vNets->nSize; i++ )
-        {
-            if ( i == 0 )
-                printf( "%s", vNets->pArray[i] );
-            else if ( i == 1 )
-                printf( ", %s", vNets->pArray[i] );
-            else if ( i == 2 )
-            {
-                printf( ", %s, etc.", vNets->pArray[i] );
-                break;
-            }
-        }
-        printf( "\n" );
-    }
-    Vec_PtrFree( vNets );
-}
-
-
-
-
-/**Function*************************************************************
-
   Synopsis    [Creates a new Obj.]
 
   Description []
@@ -1404,4 +869,3 @@ bool Abc_NodeIsInv( Abc_Obj_t * pNode )
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-
diff --git a/src/base/abc/module.make b/src/base/abc/module.make
index 695e056b..649e71a2 100644
--- a/src/base/abc/module.make
+++ b/src/base/abc/module.make
@@ -1,40 +1,15 @@
-SRC +=    src/base/abc/abc.c \
-    src/base/abc/abcAig.c \
-    src/base/abc/abcAttach.c \
-    src/base/abc/abcBalance.c \
+SRC +=    src/base/abc/abcAig.c \
     src/base/abc/abcCheck.c \
-    src/base/abc/abcCollapse.c \
-    src/base/abc/abcCreate.c \
-    src/base/abc/abcCut.c \
     src/base/abc/abcDfs.c \
-    src/base/abc/abcDsd.c \
     src/base/abc/abcFanio.c \
-    src/base/abc/abcFpga.c \
-    src/base/abc/abcFraig.c \
     src/base/abc/abcFunc.c \
-        src/base/abc/abcFxu.c \
     src/base/abc/abcLatch.c \
-    src/base/abc/abcMap.c \
     src/base/abc/abcMinBase.c \
-    src/base/abc/abcMiter.c \
     src/base/abc/abcNames.c \
     src/base/abc/abcNetlist.c \
-    src/base/abc/abcNtbdd.c \
-    src/base/abc/abcPrint.c \
-    src/base/abc/abcReconv.c \
-    src/base/abc/abcRefactor.c \
+    src/base/abc/abcNtk.c \
+    src/base/abc/abcObj.c \
     src/base/abc/abcRefs.c \
-    src/base/abc/abcRenode.c \
-    src/base/abc/abcRewrite.c \
-    src/base/abc/abcSat.c \
-    src/base/abc/abcSeq.c \
-    src/base/abc/abcSeqRetime.c \
     src/base/abc/abcShow.c \
     src/base/abc/abcSop.c \
-    src/base/abc/abcStrash.c \
-    src/base/abc/abcSweep.c \
-    src/base/abc/abcSymm.c \
-    src/base/abc/abcTiming.c \
-    src/base/abc/abcUnreach.c \
-    src/base/abc/abcUtil.c \
-    src/base/abc/abcVerify.c 
+    src/base/abc/abcUtil.c
diff --git a/src/base/abc/abc.c b/src/base/abci/abc.c
index dca80ca5..30047d23 100644
--- a/src/base/abc/abc.c
+++ b/src/base/abci/abc.c
@@ -65,6 +65,7 @@ static int Abc_CommandOneOutput    ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandOneNode      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandShortNames   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCut          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTest         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandFraig        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFraigTrust   ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -140,6 +141,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "one_node",      Abc_CommandOneNode,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "short_names",   Abc_CommandShortNames,       0 );
     Cmd_CommandAdd( pAbc, "Various",      "cut",           Abc_CommandCut,              0 );
+    Cmd_CommandAdd( pAbc, "Various",      "test",          Abc_CommandTest,             0 );
 
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_trust",   Abc_CommandFraigTrust,       1 );
@@ -591,10 +593,11 @@ usage:
 ***********************************************************************/
 int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    Vec_Ptr_t * vSuppFun;
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
-    extern void * Sim_ComputeSupp( Abc_Ntk_t * pNtk );
+    extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -619,12 +622,20 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    if ( !Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "This command works only for combinational networks.\n" );
+        return 1;
+    }
+
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "This command works only for AIGs.\n" );
         return 1;
     }
-    Sim_ComputeSupp( pNtk );
+    vSuppFun = Sim_ComputeFunSupp( pNtk );
+    free( vSuppFun->pArray[0] );
+    Vec_PtrFree( vSuppFun );
     return 0;
 
 usage:
@@ -660,7 +671,7 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fUseBdds = 1;
+    fUseBdds = 0;
     fNaive   = 0;
     fVerbose = 0;
     util_getopt_reset();
@@ -688,6 +699,11 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+    if ( !Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "This command works only for combinational networks.\n" );
+        return 1;
+    }
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "This command works only for AIGs.\n" );
@@ -2758,6 +2774,62 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    // run the command
+    pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: test [-h]\n" );
+    fprintf( pErr, "\t         testbench for new procedures\n" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 
 
@@ -3249,10 +3321,11 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     char Buffer[100];
     double DelayTarget;
     int fRecovery;
-    int fVerbose;
     int fSweep;
+    int fSwitching;
+    int fVerbose;
     int c;
-    extern Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fSwitching, int fVerbose );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -3262,9 +3335,10 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     DelayTarget =-1;
     fRecovery   = 1;
     fSweep      = 1;
+    fSwitching  = 0;
     fVerbose    = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "Dasvh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "Daspvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -3285,6 +3359,9 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             fSweep ^= 1;
             break;
+        case 'p':
+            fSwitching ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -3318,7 +3395,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
         fprintf( pOut, "The network was strashed and balanced before mapping.\n" );
         // get the new network
-        pNtkRes = Abc_NtkMap( pNtk, DelayTarget, fRecovery, fVerbose );
+        pNtkRes = Abc_NtkMap( pNtk, DelayTarget, fRecovery, fSwitching, fVerbose );
         if ( pNtkRes == NULL )
         {
             Abc_NtkDelete( pNtk );
@@ -3330,7 +3407,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     else
     {
         // get the new network
-        pNtkRes = Abc_NtkMap( pNtk, DelayTarget, fRecovery, fVerbose );
+        pNtkRes = Abc_NtkMap( pNtk, DelayTarget, fRecovery, fSwitching, fVerbose );
         if ( pNtkRes == NULL )
         {
             fprintf( pErr, "Mapping has failed.\n" );
@@ -3350,11 +3427,12 @@ usage:
         sprintf( Buffer, "not used" );
     else
         sprintf( Buffer, "%.3f", DelayTarget );
-    fprintf( pErr, "usage: map [-D num] [-asvh]\n" );
+    fprintf( pErr, "usage: map [-D num] [-aspvh]\n" );
     fprintf( pErr, "\t         performs standard cell mapping of the current network\n" );
     fprintf( pErr, "\t-D num : sets the global required times [default = %s]\n", Buffer );  
     fprintf( pErr, "\t-a     : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" );
     fprintf( pErr, "\t-s     : toggles sweep after mapping [default = %s]\n", fSweep? "yes": "no" );
+    fprintf( pErr, "\t-p     : optimizes power by minimizing switching activity [default = %s]\n", fSwitching? "yes": "no" );
     fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -3569,8 +3647,9 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
     int fRecovery;
+    int fSwitching;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fSwitching, int fVerbose );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -3578,15 +3657,19 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     fRecovery  = 1;
+    fSwitching = 0;
     fVerbose   = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "avh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "apvh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'a':
             fRecovery ^= 1;
             break;
+        case 'p':
+            fSwitching ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -3621,7 +3704,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
         fprintf( pOut, "The network was strashed and balanced before FPGA mapping.\n" );
         // get the new network
-        pNtkRes = Abc_NtkFpga( pNtk, fRecovery, fVerbose );
+        pNtkRes = Abc_NtkFpga( pNtk, fRecovery, fSwitching, fVerbose );
         if ( pNtkRes == NULL )
         {
             Abc_NtkDelete( pNtk );
@@ -3633,7 +3716,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     else
     {
         // get the new network
-        pNtkRes = Abc_NtkFpga( pNtk, fRecovery, fVerbose );
+        pNtkRes = Abc_NtkFpga( pNtk, fRecovery, fSwitching, fVerbose );
         if ( pNtkRes == NULL )
         {
             fprintf( pErr, "FPGA mapping has failed.\n" );
@@ -3645,9 +3728,10 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: fpga [-avh]\n" );
+    fprintf( pErr, "usage: fpga [-apvh]\n" );
     fprintf( pErr, "\t        performs FPGA mapping of the current network\n" );
     fprintf( pErr, "\t-a    : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" );
+    fprintf( pErr, "\t-p    : optimizes power by minimizing switching activity [default = %s]\n", fSwitching? "yes": "no" );
     fprintf( pErr, "\t-v    : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h    : prints the command usage\n");
     return 1;
diff --git a/src/base/abc/abcAttach.c b/src/base/abci/abcAttach.c
index a8e06555..a8e06555 100644
--- a/src/base/abc/abcAttach.c
+++ b/src/base/abci/abcAttach.c
diff --git a/src/base/abc/abcBalance.c b/src/base/abci/abcBalance.c
index 7deab3ba..5042d0d5 100644
--- a/src/base/abc/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -25,8 +25,8 @@
 ////////////////////////////////////////////////////////////////////////
  
 static void        Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate );
-static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, bool fDuplicate );
-static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, int fDuplicate );
+static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Vec_t * vStorage, bool fDuplicate );
+static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int fDuplicate );
 static int         Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate );
 
 ////////////////////////////////////////////////////////////////////////
@@ -78,6 +78,7 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica
 {
     int fCheck = 1;
     ProgressBar * pProgress;
+    Vec_Vec_t * vStorage;
     Abc_Obj_t * pNode, * pDriver;
     int i;
 
@@ -85,6 +86,8 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica
     Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkAig->pManFunc);
     // set the level of PIs of AIG according to the arrival times of the old network
     Abc_NtkSetNodeLevelsArrival( pNtk );
+    // allocate temporary storage for supergates
+    vStorage = Vec_VecStart( Abc_AigGetLevelNum(pNtk) + 1 );
     // perform balancing of POs
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
     Abc_NtkForEachCo( pNtk, pNode, i )
@@ -92,9 +95,10 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica
         Extra_ProgressBarUpdate( pProgress, i, NULL );
         // strash the driver node
         pDriver = Abc_ObjFanin0(pNode);
-        Abc_NodeBalance_rec( pNtkAig, pDriver, fDuplicate );
+        Abc_NodeBalance_rec( pNtkAig, pDriver, vStorage, fDuplicate );
     }
     Extra_ProgressBarStop( pProgress );
+    Vec_VecFree( vStorage );
 }
 
 /**Function*************************************************************
@@ -108,7 +112,7 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, bool fDuplicate )
+Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_Vec_t * vStorage, bool fDuplicate )
 {
     Abc_Aig_t * pMan = pNtkNew->pManFunc;
     Abc_Obj_t * pNodeNew, * pNode1, * pNode2;
@@ -120,17 +124,16 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, bool
         return pNodeOld->pCopy;
     assert( Abc_ObjIsNode(pNodeOld) );
     // get the implication supergate
-    vSuper = Abc_NodeBalanceCone( pNodeOld, fDuplicate );
+    vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, fDuplicate );
     if ( vSuper->nSize == 0 )
     { // it means that the supergate contains two nodes in the opposite polarity
-        Vec_PtrFree( vSuper );
         pNodeOld->pCopy = Abc_ObjNot(Abc_AigConst1(pMan));
         return pNodeOld->pCopy;
     }
     // for each old node, derive the new well-balanced node
     for ( i = 0; i < vSuper->nSize; i++ )
     {
-        pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), fDuplicate );
+        pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), vStorage, fDuplicate );
         vSuper->pArray[i] = Abc_ObjNotCond( pNodeNew, Abc_ObjIsComplement(vSuper->pArray[i]) );
     }
     // sort the new nodes by level in the decreasing order
@@ -147,7 +150,6 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, bool
     assert( pNodeOld->pCopy == NULL );
     // mark the old node with the new node
     pNodeOld->pCopy = vSuper->pArray[0];
-    Vec_PtrFree( vSuper );
     return pNodeOld->pCopy;
 }
 
@@ -164,12 +166,13 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, bool
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, int fDuplicate )
+Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int fDuplicate )
 {
     Vec_Ptr_t * vNodes;
     int RetValue, i;
     assert( !Abc_ObjIsComplement(pNode) );
-    vNodes = Vec_PtrAlloc( 4 );
+    vNodes = Vec_VecEntry( vStorage, pNode->Level );
+    Vec_PtrClear( vNodes );
     RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, fDuplicate );
     assert( vNodes->nSize > 0 );
     for ( i = 0; i < vNodes->nSize; i++ )
diff --git a/src/base/abc/abcCollapse.c b/src/base/abci/abcCollapse.c
index 4e359506..4e359506 100644
--- a/src/base/abc/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
diff --git a/src/base/abc/abcCut.c b/src/base/abci/abcCut.c
index f487bd1b..f487bd1b 100644
--- a/src/base/abc/abcCut.c
+++ b/src/base/abci/abcCut.c
diff --git a/src/base/abc/abcDsd.c b/src/base/abci/abcDsd.c
index 013b7ac4..013b7ac4 100644
--- a/src/base/abc/abcDsd.c
+++ b/src/base/abci/abcDsd.c
diff --git a/src/base/abc/abcFpga.c b/src/base/abci/abcFpga.c
index ad411aa5..f30325c0 100644
--- a/src/base/abc/abcFpga.c
+++ b/src/base/abci/abcFpga.c
@@ -25,7 +25,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose );
+static Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, float * pSwitching, int fVerbose );
 static Abc_Ntk_t *  Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk );
 static Abc_Obj_t *  Abc_NodeFromFpga_rec( Abc_Ntk_t * pNtkNew, Fpga_Node_t * pNodeFpga );
  
@@ -44,11 +44,14 @@ static Abc_Obj_t *  Abc_NodeFromFpga_rec( Abc_Ntk_t * pNtkNew, Fpga_Node_t * pNo
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
+Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fSwitching, int fVerbose )
 {
     int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
     Fpga_Man_t * pMan;
+    Vec_Int_t * vSwitching;
+    float * pSwitching = NULL;
+    int fShowSwitching = 0;
 
     assert( Abc_NtkIsStrash(pNtk) );
 
@@ -56,10 +59,21 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Performing FPGA mapping with choices.\n" );
 
+    // compute switching activity
+    fShowSwitching |= fSwitching;
+    if ( fShowSwitching )
+    {
+        extern Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns );
+        vSwitching = Sim_NtkComputeSwitching( pNtk, 4096 );
+        pSwitching = (float *)vSwitching->pArray;
+    }
+
     // perform FPGA mapping
-    pMan = Abc_NtkToFpga( pNtk, fRecovery, fVerbose );    
+    pMan = Abc_NtkToFpga( pNtk, fRecovery, pSwitching, fVerbose );    
+    if ( pSwitching ) Vec_IntFree( vSwitching );
     if ( pMan == NULL )
         return NULL;
+    Fpga_ManSetSwitching( pMan, fSwitching );
     if ( !Fpga_Mapping( pMan ) )
     {
         Fpga_ManFree( pMan );
@@ -96,7 +110,7 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
+Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, float * pSwitching, int fVerbose )
 {
     Fpga_Man_t * pMan;
     ProgressBar * pProgress;
@@ -118,7 +132,12 @@ Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
     // create PIs and remember them in the old nodes
     Abc_NtkCleanCopy( pNtk );
     Abc_NtkForEachCi( pNtk, pNode, i )
-        pNode->pCopy = (Abc_Obj_t *)Fpga_ManReadInputs(pMan)[i];
+    {
+        pNodeFpga = Fpga_ManReadInputs(pMan)[i];
+        pNode->pCopy = (Abc_Obj_t *)pNodeFpga;
+        if ( pSwitching )
+            Fpga_NodeSetSwitching( pNodeFpga, pSwitching[pNode->Id] );
+    }
 
     // load the AIG into the mapper
     vNodes = Abc_AigDfs( pNtk, 0, 0 );
@@ -139,6 +158,8 @@ Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
         assert( pNode->pCopy == NULL );
         // remember the node
         pNode->pCopy = (Abc_Obj_t *)pNodeFpga;
+        if ( pSwitching )
+            Fpga_NodeSetSwitching( pNodeFpga, pSwitching[pNode->Id] );
         // set up the choice node
         if ( Abc_NodeIsAigChoice( pNode ) )
             for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
@@ -197,8 +218,8 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
     Abc_NtkFinalize( pNtk, pNtkNew );
     // decouple the PO driver nodes to reduce the number of levels
     nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
-    if ( nDupGates && Fpga_ManReadVerbose(pMan) )
-        printf( "Duplicated %d gates to decouple the PO drivers.\n", nDupGates );
+//    if ( nDupGates && Fpga_ManReadVerbose(pMan) )
+//        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
     return pNtkNew;
 }
 
diff --git a/src/base/abc/abcFraig.c b/src/base/abci/abcFraig.c
index ef4746d5..fbe676a3 100644
--- a/src/base/abc/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -52,12 +52,13 @@ static Abc_Obj_t *   Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
 Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
 {
     int fCheck = 1;
+    Fraig_Params_t * pPars = pParams;
     Abc_Ntk_t * pNtkNew;
     Fraig_Man_t * pMan;
     // perform fraiging
     pMan = Abc_NtkToFraig( pNtk, pParams, fAllNodes ); 
     // prove the miter if asked to
-    if ( ((Fraig_Params_t *)pParams)->fTryProve )
+    if ( pPars->fTryProve )
         Fraig_ManProveMiter( pMan );
     // reconstruct FRAIG in the new network
     pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
@@ -106,10 +107,12 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
 
     // perform strashing
     vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
-    pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
+    if ( !pParams->fInternal )
+        pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( !pParams->fInternal )
+            Extra_ProgressBarUpdate( pProgress, i, NULL );
         if ( pNode == pConst1 )
             pNodeFraig = Fraig_ManReadConst1(pMan);
         else if ( pNode == pReset )
@@ -121,12 +124,13 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
         assert( pNode->pCopy == NULL );
         pNode->pCopy = (Abc_Obj_t *)pNodeFraig;
     }
-    Extra_ProgressBarStop( pProgress );
+    if ( !pParams->fInternal )
+        Extra_ProgressBarStop( pProgress );
     Vec_PtrFree( vNodes );
 
     // set the primary outputs
     Abc_NtkForEachCo( pNtk, pNode, i )
-        Fraig_ManSetPo( pMan, (Fraig_Node_t *)Abc_ObjFanin0(pNode)->pCopy );
+        Fraig_ManSetPo( pMan, (Fraig_Node_t *)Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) );
     return pMan;
 }
 
@@ -145,7 +149,7 @@ Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
 {
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pNode;//, * pNodeNew;
+    Abc_Obj_t * pNode, * pNodeNew;
     int i;
     // create the new network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG );
@@ -159,11 +163,10 @@ Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
-        Abc_ObjFanin0(pNode)->pCopy = Abc_NodeFromFraig_rec( pNtkNew, Fraig_ManReadOutputs(pMan)[i] );
+        pNodeNew = Abc_NodeFromFraig_rec( pNtkNew, Fraig_ManReadOutputs(pMan)[i] );
+        Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
     }
     Extra_ProgressBarStop( pProgress );
-    // finalize the new network
-    Abc_NtkFinalize( pNtk, pNtkNew );
     return pNtkNew;
 }
 
diff --git a/src/base/abc/abcFxu.c b/src/base/abci/abcFxu.c
index 0c8994e1..0c8994e1 100644
--- a/src/base/abc/abcFxu.c
+++ b/src/base/abci/abcFxu.c
diff --git a/src/base/abc/abcMap.c b/src/base/abci/abcMap.c
index 28853c8d..45f600ed 100644
--- a/src/base/abc/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -27,7 +27,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Map_Man_t *  Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fVerbose );
+static Map_Man_t *  Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, float * pSwitching, int fVerbose );
 static Abc_Ntk_t *  Abc_NtkFromMap( Map_Man_t * pMan, Abc_Ntk_t * pNtk );
 static Abc_Obj_t *  Abc_NodeFromMap_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int fPhase );
 static Abc_Obj_t *  Abc_NodeFromMapPhase_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int fPhase );
@@ -54,11 +54,14 @@ static Abc_Obj_t *  Abc_NodeFromMapSuperChoice_rec( Abc_Ntk_t * pNtkNew, Map_Sup
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fVerbose )
+Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fSwitching, int fVerbose )
 {
     int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
     Map_Man_t * pMan;
+    Vec_Int_t * vSwitching;
+    float * pSwitching = NULL;
+    int fShowSwitching = 0;
     int clk;
 
     assert( Abc_NtkIsStrash(pNtk) );
@@ -82,11 +85,22 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Performing mapping with choices.\n" );
 
+    // compute switching activity
+    fShowSwitching |= fSwitching;
+    if ( fShowSwitching )
+    {
+        extern Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns );
+        vSwitching = Sim_NtkComputeSwitching( pNtk, 4096 );
+        pSwitching = (float *)vSwitching->pArray;
+    }
+
     // perform the mapping
-    pMan = Abc_NtkToMap( pNtk, DelayTarget, fRecovery, fVerbose );
+    pMan = Abc_NtkToMap( pNtk, DelayTarget, fRecovery, pSwitching, fVerbose );
+    if ( pSwitching ) Vec_IntFree( vSwitching );
     if ( pMan == NULL )
         return NULL;
 clk = clock();
+    Map_ManSetSwitching( pMan, fSwitching );
     if ( !Map_Mapping( pMan ) )
     {
         Map_ManFree( pMan );
@@ -121,7 +135,7 @@ clk = clock();
   SeeAlso     []
 
 ***********************************************************************/
-Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fVerbose )
+Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, float * pSwitching, int fVerbose )
 {
     Map_Man_t * pMan;
     ProgressBar * pProgress;
@@ -144,7 +158,12 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, i
     // create PIs and remember them in the old nodes
     Abc_NtkCleanCopy( pNtk );
     Abc_NtkForEachCi( pNtk, pNode, i )
-        pNode->pCopy = (Abc_Obj_t *)Map_ManReadInputs(pMan)[i];
+    {
+        pNodeMap = Map_ManReadInputs(pMan)[i];
+        pNode->pCopy = (Abc_Obj_t *)pNodeMap;
+        if ( pSwitching )
+            Map_NodeSetSwitching( pNodeMap, pSwitching[pNode->Id] );
+    }
 
     // load the AIG into the mapper
     vNodes = Abc_AigDfs( pNtk, 0, 0 );
@@ -165,6 +184,8 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, i
         assert( pNode->pCopy == NULL );
         // remember the node
         pNode->pCopy = (Abc_Obj_t *)pNodeMap;
+        if ( pSwitching )
+            Map_NodeSetSwitching( pNodeMap, pSwitching[pNode->Id] );
         // set up the choice node
         if ( Abc_NodeIsAigChoice( pNode ) )
             for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
@@ -224,8 +245,8 @@ Abc_Ntk_t * Abc_NtkFromMap( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
     Extra_ProgressBarStop( pProgress );
     // decouple the PO driver nodes to reduce the number of levels
     nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
-    if ( nDupGates && Map_ManReadVerbose(pMan) )
-        printf( "Duplicated %d gates to decouple the PO drivers.\n", nDupGates );
+//    if ( nDupGates && Map_ManReadVerbose(pMan) )
+//        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
     return pNtkNew;
 }
 
@@ -446,7 +467,7 @@ Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk )
         printf( "Performing mapping with choices.\n" );
 
     // perform the mapping
-    pMan = Abc_NtkToMap( pNtk, -1, 1, 0 );
+    pMan = Abc_NtkToMap( pNtk, -1, 1, NULL, 0 );
     if ( pMan == NULL )
         return NULL;
     if ( !Map_Mapping( pMan ) )
diff --git a/src/base/abc/abcMiter.c b/src/base/abci/abcMiter.c
index a0426dc2..0d75ba1f 100644
--- a/src/base/abc/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -27,7 +27,7 @@
 static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 static void        Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
 static void        Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter );
-static void        Abc_NtkMiterAddOneNode( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
+static void        Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
 static void        Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
 static void        Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame, Vec_Ptr_t * vNodes );
 
@@ -121,8 +121,8 @@ void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtk
     Abc_Obj_t * pObj, * pObjNew;
     int i;
     // clean the copy field in all objects
-    Abc_NtkCleanCopy( pNtk1 );
-    Abc_NtkCleanCopy( pNtk2 );
+//    Abc_NtkCleanCopy( pNtk1 );
+//    Abc_NtkCleanCopy( pNtk2 );
     if ( fComb )
     {
         // create new PIs and remember them in the old PIs
@@ -224,7 +224,7 @@ void Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkMiterAddOneNode( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pRoot )
+void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pRoot )
 {
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNode, * pNodeNew, * pConst1, * pConst1New;
@@ -310,7 +310,7 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkMiterOne( Abc_Ntk_t * pNtk, int Out, int In1, int In2 )
+Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 )
 {
     int fCheck = 1;
     char Buffer[100];
@@ -324,7 +324,7 @@ Abc_Ntk_t * Abc_NtkMiterOne( Abc_Ntk_t * pNtk, int Out, int In1, int In2 )
 
     // start the new network
     pNtkMiter = Abc_NtkAlloc( ABC_TYPE_STRASH, ABC_FUNC_AIG );
-    sprintf( Buffer, "%s_%s_miter", pNtk->pName, Abc_ObjName(Abc_NtkCo(pNtk, Out)) );
+    sprintf( Buffer, "%s_miter", Abc_ObjName(Abc_NtkCo(pNtk, Out)) );
     pNtkMiter->pName = util_strsav(Buffer);
 
     // get the root output
@@ -337,7 +337,7 @@ Abc_Ntk_t * Abc_NtkMiterOne( Abc_Ntk_t * pNtk, int Out, int In1, int In2 )
     if ( In2 >= 0 )
     Abc_NtkCi(pNtk, In2)->pCopy = Abc_AigConst1( pNtkMiter->pManFunc );
     // add the first cofactor
-    Abc_NtkMiterAddOneNode( pNtk, pNtkMiter, pRoot );
+    Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
 
     // save the output
     pOutput1 = Abc_ObjFanin0(pRoot)->pCopy;
@@ -347,7 +347,7 @@ Abc_Ntk_t * Abc_NtkMiterOne( Abc_Ntk_t * pNtk, int Out, int In1, int In2 )
     if ( In2 >= 0 )
     Abc_NtkCi(pNtk, In2)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter->pManFunc) );
     // add the second cofactor
-    Abc_NtkMiterAddOneNode( pNtk, pNtkMiter, pRoot );
+    Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
 
     // save the output
     pOutput2 = Abc_ObjFanin0(pRoot)->pCopy;
diff --git a/src/base/abc/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 61c1a110..61c1a110 100644
--- a/src/base/abc/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
diff --git a/src/base/abc/abcPrint.c b/src/base/abci/abcPrint.c
index 41b9288e..41b9288e 100644
--- a/src/base/abc/abcPrint.c
+++ b/src/base/abci/abcPrint.c
diff --git a/src/base/abc/abcReconv.c b/src/base/abci/abcReconv.c
index 766c14f3..766c14f3 100644
--- a/src/base/abc/abcReconv.c
+++ b/src/base/abci/abcReconv.c
diff --git a/src/base/abc/abcRefactor.c b/src/base/abci/abcRefactor.c
index 791d2d53..791d2d53 100644
--- a/src/base/abc/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
diff --git a/src/base/abc/abcRenode.c b/src/base/abci/abcRenode.c
index c77c0d70..c77c0d70 100644
--- a/src/base/abc/abcRenode.c
+++ b/src/base/abci/abcRenode.c
diff --git a/src/base/abc/abcRewrite.c b/src/base/abci/abcRewrite.c
index 75fe1627..75fe1627 100644
--- a/src/base/abc/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
diff --git a/src/base/abc/abcSat.c b/src/base/abci/abcSat.c
index 4fb059e5..4fb059e5 100644
--- a/src/base/abc/abcSat.c
+++ b/src/base/abci/abcSat.c
diff --git a/src/base/abc/abcStrash.c b/src/base/abci/abcStrash.c
index 935f1300..935f1300 100644
--- a/src/base/abc/abcStrash.c
+++ b/src/base/abci/abcStrash.c
diff --git a/src/base/abc/abcSweep.c b/src/base/abci/abcSweep.c
index ca9bd34e..ca9bd34e 100644
--- a/src/base/abc/abcSweep.c
+++ b/src/base/abci/abcSweep.c
diff --git a/src/base/abc/abcSymm.c b/src/base/abci/abcSymm.c
index 8df3a837..f9229639 100644
--- a/src/base/abc/abcSymm.c
+++ b/src/base/abci/abcSymm.c
@@ -25,6 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
  
 static void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose );
+static void Abc_NtkSymmetriesUsingSandS( Abc_Ntk_t * pNtk, int fVerbose );
 static void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVerbose );
 static void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms );
 
@@ -48,7 +49,25 @@ void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose
     if ( fUseBdds || fNaive )
         Abc_NtkSymmetriesUsingBdds( pNtk, fNaive, fVerbose );
     else
-        printf( "This option is currently not implemented.\n" );
+        Abc_NtkSymmetriesUsingSandS( pNtk, fVerbose );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Symmetry computation using simulation and SAT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSymmetriesUsingSandS( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    extern int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk );
+    int nSymms = Sim_ComputeTwoVarSymms( pNtk );
+    printf( "The total number of symmetries is %d.\n", nSymms );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abc/abcTiming.c b/src/base/abci/abcTiming.c
index b8524bd5..b8524bd5 100644
--- a/src/base/abc/abcTiming.c
+++ b/src/base/abci/abcTiming.c
diff --git a/src/base/abc/abcUnreach.c b/src/base/abci/abcUnreach.c
index 0fe3ec63..0fe3ec63 100644
--- a/src/base/abc/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
diff --git a/src/base/abc/abcVerify.c b/src/base/abci/abcVerify.c
index 55d6cf7d..55d6cf7d 100644
--- a/src/base/abc/abcVerify.c
+++ b/src/base/abci/abcVerify.c
diff --git a/src/base/abci/abc_.c b/src/base/abci/abc_.c
new file mode 100644
index 00000000..bef3836f
--- /dev/null
+++ b/src/base/abci/abc_.c
@@ -0,0 +1,47 @@
+/**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"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
new file mode 100644
index 00000000..d7c0add2
--- /dev/null
+++ b/src/base/abci/module.make
@@ -0,0 +1,24 @@
+SRC +=    src/base/abci/abc.c \
+    src/base/abci/abcAttach.c \
+    src/base/abci/abcBalance.c \
+    src/base/abci/abcCollapse.c \
+    src/base/abci/abcCut.c \
+    src/base/abci/abcDsd.c \
+    src/base/abci/abcFpga.c \
+    src/base/abci/abcFraig.c \
+        src/base/abci/abcFxu.c \
+    src/base/abci/abcMap.c \
+    src/base/abci/abcMiter.c \
+    src/base/abci/abcNtbdd.c \
+    src/base/abci/abcPrint.c \
+    src/base/abci/abcReconv.c \
+    src/base/abci/abcRefactor.c \
+    src/base/abci/abcRenode.c \
+    src/base/abci/abcRewrite.c \
+    src/base/abci/abcSat.c \
+    src/base/abci/abcStrash.c \
+    src/base/abci/abcSweep.c \
+    src/base/abci/abcSymm.c \
+    src/base/abci/abcTiming.c \
+    src/base/abci/abcUnreach.c \
+    src/base/abci/abcVerify.c 
diff --git a/src/base/abc/abcSeqRetime.c b/src/base/abcs/abcRetime.c
index 13b8a926..13b8a926 100644
--- a/src/base/abc/abcSeqRetime.c
+++ b/src/base/abcs/abcRetime.c
diff --git a/src/base/abc/abcSeq.c b/src/base/abcs/abcSeq.c
index d6b1b8e5..d6b1b8e5 100644
--- a/src/base/abc/abcSeq.c
+++ b/src/base/abcs/abcSeq.c
diff --git a/src/base/abcs/abc_.c b/src/base/abcs/abc_.c
new file mode 100644
index 00000000..bef3836f
--- /dev/null
+++ b/src/base/abcs/abc_.c
@@ -0,0 +1,47 @@
+/**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"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abcs/module.make b/src/base/abcs/module.make
new file mode 100644
index 00000000..ad084bb8
--- /dev/null
+++ b/src/base/abcs/module.make
@@ -0,0 +1,2 @@
+SRC +=    src/base/abcs/abcRetime.c \
+    src/base/abcs/abcSeq.c
diff --git a/src/base/io/ioWriteDot_old.c b/src/base/io/ioWriteDot_old.c
deleted file mode 100644
index 59bbbde3..00000000
--- a/src/base/io/ioWriteDot_old.c
+++ /dev/null
@@ -1,325 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [ioWriteDot.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Command processing package.]
-
-  Synopsis    [Procedures to write the graph structure of AIG in DOT.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: ioWriteDot.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "io.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Writes the graph structure of AIG in DOT.]
-
-  Description [Useful for graph visualization using tools such as GraphViz: 
-  http://www.graphviz.org/]
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName )
-{
-    FILE * pFile;
-    Abc_Obj_t * pNode, * pFanin, * pPrev, * pTemp;
-    int LevelMin, LevelMax, fHasCos, Level, i;
-    int Limit = 200;
-
-    if ( vNodes->nSize < 1 )
-    {
-        printf( "The set has no nodes. DOT file is not written.\n" );
-        return;
-    }
-
-    if ( vNodes->nSize > Limit )
-    {
-        printf( "The set has more than %d nodes. DOT file is not written.\n", Limit );
-        return;
-    }
-
-    // start the output file
-    if ( (pFile = fopen( pFileName, "w" )) == NULL )
-    {
-        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName );
-        return;
-    }
-
-    // mark the nodes from the set
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-        pNode->fMarkC = 1;
-    if ( vNodesShow )
-        Vec_PtrForEachEntry( vNodesShow, pNode, i )
-            pNode->fMarkB = 1;
-
-    // find the largest and the smallest levels
-    LevelMin = 10000;
-    LevelMax = -1;
-    fHasCos  = 0;
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-    {
-        if ( Abc_ObjIsCo(pNode) )
-        {
-            fHasCos = 1;
-            continue;
-        }
-        if ( LevelMin > (int)pNode->Level )
-            LevelMin = pNode->Level;
-        if ( LevelMax < (int)pNode->Level )
-            LevelMax = pNode->Level;
-    }
-
-    // set the level of the CO nodes
-    if ( fHasCos )
-    {
-        LevelMax++;
-        Vec_PtrForEachEntry( vNodes, pNode, i )
-        {
-            if ( Abc_ObjIsCo(pNode) )
-                pNode->Level = LevelMax;
-        }
-    }
-
-    // write the DOT header
-    fprintf( pFile, "# %s\n",  "AIG generated by ABC" );
-    fprintf( pFile, "\n" );
-    fprintf( pFile, "digraph AIG {\n" );
-    fprintf( pFile, "size = \"7.5,10\";\n" );
-//  fprintf( pFile, "ranksep = 0.5;\n" );
-//  fprintf( pFile, "nodesep = 0.5;\n" );
-    fprintf( pFile, "center = true;\n" );
-//  fprintf( pFile, "edge [fontsize = 10];\n" );
-//    fprintf( pFile, "edge [dir = back];\n" );
-//  fprintf( pFile, "edge [dir = none];\n" );
-    fprintf( pFile, "\n" );
-
-    // labels on the left of the picture
-    fprintf( pFile, "{\n" );
-    fprintf( pFile, "  node [shape = plaintext];\n" );
-    fprintf( pFile, "  edge [style = invis];\n" );
-    fprintf( pFile, "  LevelTitle1 [label=\"\"];\n" );
-    fprintf( pFile, "  LevelTitle2 [label=\"\"];\n" );
-    // generate node names with labels
-    for ( Level = LevelMax; Level >= LevelMin; Level-- )
-    {
-        // the visible node name
-        fprintf( pFile, "  Level%d", Level );
-        fprintf( pFile, " [label = " );
-        // label name
-        fprintf( pFile, "\"" );
-        fprintf( pFile, "\"" );
-        fprintf( pFile, "];\n" );
-    }
-
-    // genetate the sequence of visible/invisible nodes to mark levels
-    fprintf( pFile, "  LevelTitle1 ->  LevelTitle2 ->" );
-    for ( Level = LevelMax; Level >= LevelMin; Level-- )
-    {
-        // the visible node name
-        fprintf( pFile, "  Level%d",  Level );
-        // the connector
-        if ( Level != LevelMin )
-            fprintf( pFile, " ->" );
-        else
-            fprintf( pFile, ";" );
-    }
-    fprintf( pFile, "\n" );
-    fprintf( pFile, "}" );
-    fprintf( pFile, "\n" );
-    fprintf( pFile, "\n" );
-
-    // generate title box on top
-    fprintf( pFile, "{\n" );
-    fprintf( pFile, "  rank = same;\n" );
-    fprintf( pFile, "  LevelTitle1;\n" );
-    fprintf( pFile, "  title1 [shape=plaintext,\n" );
-    fprintf( pFile, "          fontsize=20,\n" );
-    fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
-    fprintf( pFile, "          label=\"" );
-    fprintf( pFile, "%s", "AIG generated by ABC" );
-    fprintf( pFile, "\\n" );
-    fprintf( pFile, "Benchmark \\\"%s\\\". ", pNtk->pName );
-    fprintf( pFile, "Time was %s. ",  Extra_TimeStamp() );
-    fprintf( pFile, "\"\n" );
-    fprintf( pFile, "         ];\n" );
-    fprintf( pFile, "}" );
-    fprintf( pFile, "\n" );
-    fprintf( pFile, "\n" );
-
-    // generate statistics box
-    fprintf( pFile, "{\n" );
-    fprintf( pFile, "  rank = same;\n" );
-    fprintf( pFile, "  LevelTitle2;\n" );
-    fprintf( pFile, "  title2 [shape=plaintext,\n" );
-    fprintf( pFile, "          fontsize=18,\n" );
-    fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
-    fprintf( pFile, "          label=\"" );
-    fprintf( pFile, "The set contains %d nodes and spans %d levels.", vNodes->nSize, LevelMax - LevelMin );
-    fprintf( pFile, "\\n" );
-    fprintf( pFile, "\"\n" );
-    fprintf( pFile, "         ];\n" );
-    fprintf( pFile, "}" );
-    fprintf( pFile, "\n" );
-    fprintf( pFile, "\n" );
-
-    // generate the POs
-    if ( fHasCos )
-    {
-        fprintf( pFile, "{\n" );
-        fprintf( pFile, "  rank = same;\n" );
-        // the labeling node of this level
-        fprintf( pFile, "  Level%d;\n",  LevelMax );
-        // generat the PO nodes
-        Vec_PtrForEachEntry( vNodes, pNode, i )
-        {
-            if ( !Abc_ObjIsCo(pNode) )
-                continue;
-            fprintf( pFile, "  Node%d%s [label = \"%s\"", pNode->Id, (Abc_ObjIsLatch(pNode)? "Top":""), Abc_ObjName(pNode) );
-            fprintf( pFile, ", shape = invtriangle" );
-            if ( pNode->fMarkB )
-                fprintf( pFile, ", style = filled" );
-            fprintf( pFile, ", color = coral, fillcolor = coral" );
-            fprintf( pFile, "];\n" );
-        }
-        fprintf( pFile, "}" );
-        fprintf( pFile, "\n" );
-        fprintf( pFile, "\n" );
-    }
-
-    // generate nodes of each rank
-    for ( Level = LevelMax - fHasCos; Level >= LevelMin && Level > 0; Level-- )
-    {
-        fprintf( pFile, "{\n" );
-        fprintf( pFile, "  rank = same;\n" );
-        // the labeling node of this level
-        fprintf( pFile, "  Level%d;\n",  Level );
-        Vec_PtrForEachEntry( vNodes, pNode, i )
-        {
-            if ( (int)pNode->Level != Level )
-                continue;
-            fprintf( pFile, "  Node%d [label = \"%d\"", pNode->Id, pNode->Id );
-            fprintf( pFile, ", shape = ellipse" );
-            if ( pNode->fMarkB )
-                fprintf( pFile, ", style = filled" );
-            fprintf( pFile, "];\n" );
-        }
-        fprintf( pFile, "}" );
-        fprintf( pFile, "\n" );
-        fprintf( pFile, "\n" );
-    }
-
-    // generate the PI nodes if any
-    if ( LevelMin == 0 )
-    {
-        fprintf( pFile, "{\n" );
-        fprintf( pFile, "  rank = same;\n" );
-        // the labeling node of this level
-        fprintf( pFile, "  Level%d;\n",  LevelMin );
-        // generat the PO nodes
-        Vec_PtrForEachEntry( vNodes, pNode, i )
-        {
-            if ( !Abc_ObjIsCi(pNode) )
-                continue;
-            fprintf( pFile, "  Node%d%s [label = \"%s\"", pNode->Id, (Abc_ObjIsLatch(pNode)? "Bot":""), Abc_ObjName(pNode) );
-            fprintf( pFile, ", shape = triangle" );
-            if ( pNode->fMarkB )
-                fprintf( pFile, ", style = filled" );
-            fprintf( pFile, ", color = coral, fillcolor = coral" );
-            fprintf( pFile, "];\n" );
-        }
-        fprintf( pFile, "}" );
-        fprintf( pFile, "\n" );
-        fprintf( pFile, "\n" );
-    }
-
-    // generate invisible edges from the square down
-    fprintf( pFile, "title1 -> title2 [style = invis];\n" );
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-    {
-        if ( (int)pNode->Level != LevelMax )
-            continue;
-        fprintf( pFile, "title2 -> Node%d%s [style = invis];\n", pNode->Id );
-    }
-
-    // generate edges
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-    { 
-        if ( Abc_ObjFaninNum(pNode) == 0 )
-            continue;
-        // generate the edge from this node to the next
-        pFanin = Abc_ObjFanin0(pNode);
-        if ( pFanin->fMarkC )
-        {
-            fprintf( pFile, "Node%d%s", pNode->Id, (Abc_ObjIsLatch(pNode)? "Top":"") );
-            fprintf( pFile, " -> " );
-            fprintf( pFile, "Node%d%s", pFanin->Id, (Abc_ObjIsLatch(pFanin)? "Bot":"") );
-            fprintf( pFile, " [style = %s]", Abc_ObjFaninC0(pNode)? "dashed" : "bold" );
-            fprintf( pFile, ";\n" );
-        }
-        if ( Abc_ObjFaninNum(pNode) == 1 )
-            continue;
-        // generate the edge from this node to the next
-        pFanin = Abc_ObjFanin1(pNode);
-        if ( pFanin->fMarkC )
-        {
-            fprintf( pFile, "Node%d",  pNode->Id );
-            fprintf( pFile, " -> " );
-            fprintf( pFile, "Node%d%s",  pFanin->Id, (Abc_ObjIsLatch(pFanin)? "Bot":"") );
-            fprintf( pFile, " [style = %s]", Abc_ObjFaninC1(pNode)? "dashed" : "bold" );
-            fprintf( pFile, ";\n" );
-        }
-        // generate the edges between the equivalent nodes
-        pPrev = pNode;
-        for ( pTemp = pNode->pData; pTemp; pTemp = pTemp->pData )
-        {
-            if ( pTemp->fMarkC )
-            {
-                fprintf( pFile, "Node%d",  pPrev->Id );
-                fprintf( pFile, " -> " );
-                fprintf( pFile, "Node%d",  pTemp->Id );
-                fprintf( pFile, " [style = %s]", (pPrev->fPhase ^ pTemp->fPhase)? "dashed" : "bold" );
-                fprintf( pFile, ";\n" );
-                pPrev = pTemp;
-            }
-        }
-    }
-
-    fprintf( pFile, "}" );
-    fprintf( pFile, "\n" );
-    fprintf( pFile, "\n" );
-    fclose( pFile );
-
-    // unmark the nodes from the set
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-        pNode->fMarkC = 0;
-    if ( vNodesShow )
-        Vec_PtrForEachEntry( vNodesShow, pNode, i )
-            pNode->fMarkB = 0;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-