Version abc80406

33 files changed, 1328 insertions, 66 deletions

diff --git a/abc.dsp b/abc.dsp
index f6771b7f..9034256e 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -3070,6 +3070,10 @@ SOURCE=.\src\aig\ntl\ntlExtract.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\ntl\ntlFraig.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\ntl\ntlInsert.c
 # End Source File
 # Begin Source File
@@ -3098,6 +3102,10 @@ SOURCE=.\src\aig\ntl\ntlTime.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\ntl\ntlUtil.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\ntl\ntlWriteBlif.c
 # End Source File
 # End Group
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 13a82817..2231b4e7 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -312,7 +312,8 @@ static inline int          Aig_ObjLevelNew( Aig_Obj_t * pObj )    { assert( !Aig
 static inline int          Aig_ObjSetLevel( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return pObj->Level = i;                    }
 static inline void         Aig_ObjClean( Aig_Obj_t * pObj )       { memset( pObj, 0, sizeof(Aig_Obj_t) );                                                             }
 static inline Aig_Obj_t *  Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj )  { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); } 
-static inline Aig_Obj_t *  Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj )    { return p->pEquivs? p->pEquivs[pObj->Id] : NULL;             } 
+static inline Aig_Obj_t *  Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj )    { return p->pEquivs? p->pEquivs[pObj->Id] : NULL;           } 
+static inline Aig_Obj_t *  Aig_ObjRepr( Aig_Man_t * p, Aig_Obj_t * pObj )     { return p->pReprs? p->pReprs[pObj->Id] : NULL;             } 
 static inline int          Aig_ObjPioNum( Aig_Obj_t * pObj )      { assert( !Aig_ObjIsNode(pObj) ); return (int)pObj->pNext;                                                    }
 static inline int          Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )    
 { 
@@ -466,6 +467,8 @@ extern Aig_Man_t *     Aig_ManDupDfs( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder );
 extern Aig_Man_t *     Aig_ManDupLevelized( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupWithoutPos( Aig_Man_t * p );
+extern Aig_Man_t *     Aig_ManDupRepres( Aig_Man_t * p );
+extern Aig_Man_t *     Aig_ManDupRepresDfs( Aig_Man_t * p );
 /*=== aigFanout.c ==========================================================*/
 extern void            Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
 extern void            Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
@@ -599,7 +602,7 @@ extern void            Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_
 extern void            Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig );
 extern void            Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig );
 extern void            Aig_ManDump( Aig_Man_t * p );
-extern void            Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
+extern void            Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames );
 extern void            Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName );
 extern void            Aig_ManSetPioNumbers( Aig_Man_t * p );
 extern void            Aig_ManCleanPioNumbers( Aig_Man_t * p );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 34657a0b..917558c6 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -121,8 +121,8 @@ void Aig_ManDfs_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
         return;
     Aig_ObjSetTravIdCurrent(p, pObj);
-    if ( p->pEquivs && p->pEquivs[pObj->Id] )
-        Aig_ManDfs_rec( p, p->pEquivs[pObj->Id], vNodes );
+    if ( p->pEquivs && Aig_ObjEquiv(p, pObj) )
+        Aig_ManDfs_rec( p, Aig_ObjEquiv(p, pObj), vNodes );
     Aig_ManDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
     Aig_ManDfs_rec( p, Aig_ObjFanin1(pObj), vNodes );
     Vec_PtrPush( vNodes, pObj );
@@ -239,7 +239,7 @@ void Aig_ManDfsChoices_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes
     assert( Aig_ObjIsNode(pObj) );
     Aig_ManDfsChoices_rec( p, Aig_ObjFanin0(pObj), vNodes );
     Aig_ManDfsChoices_rec( p, Aig_ObjFanin1(pObj), vNodes );
-    Aig_ManDfsChoices_rec( p, p->pEquivs[pObj->Id], vNodes );
+    Aig_ManDfsChoices_rec( p, Aig_ObjEquiv(p, pObj), vNodes );
     assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
     Aig_ObjSetTravIdCurrent(p, pObj);
     Vec_PtrPush( vNodes, pObj );
@@ -411,7 +411,7 @@ void Aig_ManChoiceLevel_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
         LevelMax++;
 
         // get the level of the nodes in the choice node
-        if ( p->pEquivs && (pNext = p->pEquivs[pObj->Id]) )
+        if ( p->pEquivs && (pNext = Aig_ObjEquiv(p, pObj)) )
         {
             Aig_ManChoiceLevel_rec( p, pNext );
             if ( LevelMax < Aig_ObjLevel(pNext) )
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index 61e71c31..fb0a8ba8 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -178,8 +178,8 @@ Aig_Obj_t * Aig_ManDupDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj
     Aig_Obj_t * pObjNew, * pEquivNew = NULL;
     if ( pObj->pData )
         return pObj->pData;
-    if ( p->pEquivs && p->pEquivs[pObj->Id] )
-        pEquivNew = Aig_ManDupDfs_rec( pNew, p, p->pEquivs[pObj->Id] );
+    if ( p->pEquivs && Aig_ObjEquiv(p, pObj) )
+        pEquivNew = Aig_ManDupDfs_rec( pNew, p, Aig_ObjEquiv(p, pObj) );
     Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );
     if ( Aig_ObjIsBuf(pObj) )
         return pObj->pData = Aig_ObjChild0Copy(pObj);
@@ -482,6 +482,144 @@ Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Returns representatives of fanin in approapriate polarity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Aig_Obj_t * Aig_ObjGetRepres( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pRepr;
+    if ( (pRepr = Aig_ObjRepr(p, pObj)) )
+        return Aig_NotCond( pRepr->pData, pObj->fPhase ^ pRepr->fPhase );
+    return pObj->pData;
+}
+static inline Aig_Obj_t * Aig_ObjChild0Repres( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjGetRepres(p, Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) ); }
+static inline Aig_Obj_t * Aig_ObjChild1Repres( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjGetRepres(p, Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) ); }
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while substituting representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    // start the HOP package
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->nRegs = p->nRegs;
+    if ( p->vFlopNums )
+        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+    // map the const and primary inputs
+    Aig_ManCleanData( p );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjIsNode(pObj) )
+            pObj->pData = Aig_And( pNew, Aig_ObjChild0Repres(p, pObj), Aig_ObjChild1Repres(p, pObj) );
+        else if ( Aig_ObjIsPi(pObj) )
+            pObj->pData = Aig_ObjCreatePi(pNew);
+        else if ( Aig_ObjIsPo(pObj) )
+            pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Repres(p, pObj) );
+        else if ( Aig_ObjIsConst1(pObj) )
+            pObj->pData = Aig_ManConst1(pNew);
+        else
+            assert( 0 );
+    }
+    // check the new manager
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDupReprentative: Check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManDupRepres_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pRepr;
+    if ( pObj->pData )
+        return pObj->pData;
+    if ( (pRepr = Aig_ObjRepr(p, pObj)) )
+    {
+        Aig_ManDupRepres_rec( pNew, p, pRepr );
+        return pObj->pData = Aig_NotCond( pRepr->pData, pRepr->fPhase ^ pObj->fPhase );
+    }
+    Aig_ManDupRepres_rec( pNew, p, Aig_ObjFanin0(pObj) );
+    Aig_ManDupRepres_rec( pNew, p, Aig_ObjFanin1(pObj) );
+    return pObj->pData = Aig_And( pNew, Aig_ObjChild0Repres(p, pObj), Aig_ObjChild1Repres(p, pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while substituting representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    // start the HOP package
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->nRegs = p->nRegs;
+    if ( p->vFlopNums )
+        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+    // map the const and primary inputs
+    Aig_ManCleanData( p );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjIsNode(pObj) )
+            continue;
+        if ( Aig_ObjIsPi(pObj) )
+            pObj->pData = Aig_ObjCreatePi(pNew);
+        else if ( Aig_ObjIsPo(pObj) )
+        {
+            Aig_ManDupRepres_rec( pNew, p, Aig_ObjFanin0(pObj) );
+            pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Repres(p, pObj) );
+        }
+        else if ( Aig_ObjIsConst1(pObj) )
+            pObj->pData = Aig_ManConst1(pNew);
+        else 
+            assert( 0 );
+    }
+    // check the new manager
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDupReprentative: Check has failed.\n" );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigHaig.c b/src/aig/aig/aigHaig.c
index e465a07a..491a09a3 100644
--- a/src/aig/aig/aigHaig.c
+++ b/src/aig/aig/aigHaig.c
@@ -259,7 +259,7 @@ void Aig_ManHaigRecord( Aig_Man_t * p )
     // perform a sequence of synthesis steps
     pNew = Aig_ManRetimeFrontier( p, 10000 );
     // use the haig for verification
-    Aig_ManDumpBlif( pNew->pManHaig, "haig_temp.blif" );
+    Aig_ManDumpBlif( pNew->pManHaig, "haig_temp.blif", NULL, NULL );
     Aig_ManHaigVerify( pNew->pManHaig );
     Aig_ManStop( pNew );
 }
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index ce7221ae..52633da7 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -1376,8 +1376,7 @@ Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfM
     Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
 
     // set the PI numbers
-    Aig_ManForEachPi( pAig, pObj, k )
-        pObj->pNext = (Aig_Obj_t *)(long)k;
+    Aig_ManSetPioNumbers( pAig );
 
     // create the total fraiged AIG
     Vec_PtrForEachEntry( vParts, vPart, i )
@@ -1410,8 +1409,7 @@ Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfM
     Vec_VecFree( (Vec_Vec_t *)vParts );
 
     // clear the PI numbers
-    Aig_ManForEachPi( pAig, pObj, k )
-        pObj->pNext = NULL;
+    Aig_ManCleanPioNumbers( pAig );
 
     // derive the result of choicing
     return Aig_ManDupRepr( pAig, 0 );
@@ -1533,10 +1531,10 @@ void Aig_ManChoiceEval( Aig_Man_t * p )
             int x = 0;
         }
         Counter = 0;
-        for ( pTemp = pNode; pTemp; pTemp = p->pEquivs[pTemp->Id] )
+        for ( pTemp = pNode; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
             Counter++;
         printf( "Choice node = %5d. Level = %2d. Choices = %d. { ", pNode->Id, pNode->Level, Counter );
-        for ( pTemp = pNode; pTemp; pTemp = p->pEquivs[pTemp->Id] )
+        for ( pTemp = pNode; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
         {
             Counter = Aig_NodeMffsSupp( p, pTemp, 0, vSupp );
             printf( "S=%d N=%d L=%d  ", Vec_PtrSize(vSupp), Counter, pTemp->Level );
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 422dea47..4eefa283 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -184,15 +184,15 @@ static inline Aig_Obj_t * Aig_ObjFindReprTransitive( Aig_Man_t * p, Aig_Obj_t *
   SeeAlso     []
 
 ***********************************************************************/
-static inline Aig_Obj_t * Aig_ObjRepr( Aig_Man_t * p, Aig_Obj_t * pObj )
+static inline Aig_Obj_t * Aig_ObjGetRepr( Aig_Man_t * p, Aig_Obj_t * pObj )
 {
     Aig_Obj_t * pRepr;
     if ( (pRepr = Aig_ObjFindRepr(p, pObj)) )
         return Aig_NotCond( pRepr->pData, pObj->fPhase ^ pRepr->fPhase );
     return pObj->pData;
 }
-static inline Aig_Obj_t * Aig_ObjChild0Repr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjRepr(p, Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) ); }
-static inline Aig_Obj_t * Aig_ObjChild1Repr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjRepr(p, Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) ); }
+static inline Aig_Obj_t * Aig_ObjChild0Repr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjGetRepr(p, Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) ); }
+static inline Aig_Obj_t * Aig_ObjChild1Repr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjGetRepr(p, Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) ); }
 
 /**Function*************************************************************
 
@@ -357,7 +357,7 @@ int Aig_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pNode, Aig_Obj_t * pOld )
     if ( Aig_ObjCheckTfi_rec( p, Aig_ObjFanin1(pNode), pOld ) )
         return 1;
     // check equivalent nodes
-    return Aig_ObjCheckTfi_rec( p, p->pEquivs[pNode->Id], pOld );
+    return Aig_ObjCheckTfi_rec( p, Aig_ObjEquiv(p, pNode), pOld );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index e9382468..7dc0c6e3 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -649,7 +649,7 @@ void Aig_ManDump( Aig_Man_t * p )
     char FileName[20];
     // dump the logic into a file
     sprintf( FileName, "aigbug\\%03d.blif", ++Counter );
-    Aig_ManDumpBlif( p, FileName );
+    Aig_ManDumpBlif( p, FileName, NULL, NULL );
     printf( "Intermediate AIG with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(p), FileName );
 }
 
@@ -664,7 +664,7 @@ void Aig_ManDump( Aig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
+void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames )
 {
     FILE * pFile;
     Vec_Ptr_t * vNodes;
@@ -694,44 +694,75 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
     pFile = fopen( pFileName, "w" );
     fprintf( pFile, "# BLIF file written by procedure Aig_ManDumpBlif()\n" );
 //    fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
-    fprintf( pFile, ".model test\n" );
+    fprintf( pFile, ".model %s\n", p->pName );
     // write PIs
     fprintf( pFile, ".inputs" );
     Aig_ManForEachPiSeq( p, pObj, i )
-        fprintf( pFile, " n%0*d", nDigits, pObj->iData );
+        if ( vPiNames )
+            fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, i) );
+        else
+            fprintf( pFile, " n%0*d", nDigits, pObj->iData );
     fprintf( pFile, "\n" );
     // write POs
     fprintf( pFile, ".outputs" );
     Aig_ManForEachPoSeq( p, pObj, i )
-        fprintf( pFile, " n%0*d", nDigits, pObj->iData );
+        if ( vPoNames )
+            fprintf( pFile, " %s", Vec_PtrEntry(vPoNames, i) );
+        else
+            fprintf( pFile, " n%0*d", nDigits, pObj->iData );
     fprintf( pFile, "\n" );
     // write latches
     if ( Aig_ManRegNum(p) )
     {
         fprintf( pFile, "\n" );
         Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
-            fprintf( pFile, ".latch n%0*d n%0*d 0\n", nDigits, pObjLi->iData, nDigits, pObjLo->iData );
+        {
+            fprintf( pFile, ".latch" );
+            if ( vPoNames )
+                fprintf( pFile, " %s", Vec_PtrEntry(vPoNames, Aig_ManPoNum(p)-Aig_ManRegNum(p)+i) );
+            else
+                fprintf( pFile, " n%0*d", nDigits, pObjLi->iData );
+            if ( vPiNames )
+                fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, Aig_ManPiNum(p)-Aig_ManRegNum(p)+i) );
+            else
+                fprintf( pFile, " n%0*d", nDigits, pObjLo->iData );
+            fprintf( pFile, " 0\n" );
+        }
         fprintf( pFile, "\n" );
     } 
     // write nodes
     if ( pConst1 )
         fprintf( pFile, ".names n%0*d\n 1\n", nDigits, pConst1->iData );
+    Aig_ManSetPioNumbers( p );
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
-        fprintf( pFile, ".names n%0*d n%0*d n%0*d\n", 
-            nDigits, Aig_ObjFanin0(pObj)->iData, 
-            nDigits, Aig_ObjFanin1(pObj)->iData, 
-            nDigits, pObj->iData );
+        fprintf( pFile, ".names" );
+        if ( vPiNames && Aig_ObjIsPi(Aig_ObjFanin0(pObj)) )
+            fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, Aig_ObjPioNum(Aig_ObjFanin0(pObj))) );
+        else
+            fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData );
+        if ( vPiNames && Aig_ObjIsPi(Aig_ObjFanin1(pObj)) )
+            fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, Aig_ObjPioNum(Aig_ObjFanin1(pObj))) );
+        else
+            fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin1(pObj)->iData );
+        fprintf( pFile, " n%0*d\n", nDigits, pObj->iData );
         fprintf( pFile, "%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
     }
     // write POs
     Aig_ManForEachPo( p, pObj, i )
     {
-        fprintf( pFile, ".names n%0*d n%0*d\n", 
-            nDigits, Aig_ObjFanin0(pObj)->iData, 
-            nDigits, pObj->iData );
+        fprintf( pFile, ".names" );
+        if ( vPiNames && Aig_ObjIsPi(Aig_ObjFanin0(pObj)) )
+            fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, Aig_ObjPioNum(Aig_ObjFanin0(pObj))) );
+        else
+            fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData );
+        if ( vPoNames )
+            fprintf( pFile, " %s\n", Vec_PtrEntry(vPoNames, Aig_ObjPioNum(pObj)) );
+        else
+            fprintf( pFile, " n%0*d\n", nDigits, pObj->iData );
         fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) );
     }
+    Aig_ManCleanPioNumbers( p );
     fprintf( pFile, ".end\n\n" );
     fclose( pFile );
     Vec_PtrFree( vNodes );
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 80799e3e..75de8a71 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -155,7 +155,7 @@ static inline void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_
     pTemp = Aig_ManExtractMiter( p->pManFraig, pObjFraig, pObjReprFraig );
     // dump the logic into a file
     sprintf( FileName, "aig\\%03d.blif", ++Counter );
-    Aig_ManDumpBlif( pTemp, FileName );
+    Aig_ManDumpBlif( pTemp, FileName, NULL, NULL );
     printf( "Speculation cone with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(pTemp), FileName );
     // clean up
     Aig_ManStop( pTemp );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 03d03ea1..2dde907c 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -50,8 +50,8 @@ void Fra_FraigInductionRewrite( Fra_Man_t * p )
 //    pTemp = Dar_ManRwsat( pTemp, 1, 0 );
     pTemp = Dar_ManRewriteDefault( p->pManFraig );
 //    printf( "Before = %6d.  After = %6d.\n", Aig_ManNodeNum(p->pManFraig), Aig_ManNodeNum(pTemp) ); 
-//Aig_ManDumpBlif( p->pManFraig, "1.blif" );
-//Aig_ManDumpBlif( pTemp, "2.blif" );
+//Aig_ManDumpBlif( p->pManFraig, "1.blif", NULL, NULL );
+//Aig_ManDumpBlif( pTemp, "2.blif", NULL, NULL );
 //    Fra_FramesWriteCone( pTemp );
 //    Aig_ManStop( pTemp );
     // transfer PI/register pointers
@@ -431,7 +431,7 @@ PRT( "Time", clock() - clk );
 
     // dump AIG of the timeframes
 //    pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK );
-//    Aig_ManDumpBlif( pManAigNew, "frame_aig.blif" );
+//    Aig_ManDumpBlif( pManAigNew, "frame_aig.blif", NULL, NULL );
 //    Fra_ManPartitionTest2( pManAigNew );
 //    Aig_ManStop( pManAigNew );
  
@@ -448,7 +448,7 @@ PRT( "Time", clock() - clk );
 clk2 = clock();
         p->pManFraig = Fra_FramesWithClasses( p );
 p->timeTrav += clock() - clk2;
-//Aig_ManDumpBlif( p->pManFraig, "testaig.blif" );
+//Aig_ManDumpBlif( p->pManFraig, "testaig.blif", NULL, NULL );
 
         // perform AIG rewriting
         if ( p->pPars->fRewrite )
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 83a551b8..389c3e2f 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -59,7 +59,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fFraiging
         printf( "Original miter:       Latches = %5d. Nodes = %6d.\n", 
             Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
     }
-//Aig_ManDumpBlif( pNew, "after.blif" );
+//Aig_ManDumpBlif( pNew, "after.blif", NULL, NULL );
 
     // perform sequential cleanup
 clk = clock();
diff --git a/src/aig/hop/cudd2.c b/src/aig/hop/cudd2.c
index 28d13ce0..11842c39 100644
--- a/src/aig/hop/cudd2.c
+++ b/src/aig/hop/cudd2.c
@@ -77,7 +77,7 @@ void Cudd2_Init( unsigned int numVars, unsigned int numVarsZ, unsigned int numSl
 void Cudd2_Quit( void * pCudd )
 {
     assert( s_pCuddMan != NULL );
-    Aig_ManDumpBlif( s_pCuddMan->pAig, "aig_temp.blif" );
+    Aig_ManDumpBlif( s_pCuddMan->pAig, "aig_temp.blif", NULL, NULL );
     Aig_ManStop( s_pCuddMan->pAig );
     st_free_table( s_pCuddMan->pTable );
     free( s_pCuddMan );
diff --git a/src/aig/ntl/module.make b/src/aig/ntl/module.make
index aba4fbf2..d3f2cfdd 100644
--- a/src/aig/ntl/module.make
+++ b/src/aig/ntl/module.make
@@ -1,6 +1,7 @@
 SRC +=    src/aig/ntl/ntlCheck.c \
     src/aig/ntl/ntlCore.c \
     src/aig/ntl/ntlExtract.c \
+    src/aig/ntl/ntlFraig.c \
     src/aig/ntl/ntlInsert.c \
     src/aig/ntl/ntlMan.c \
     src/aig/ntl/ntlMap.c \
@@ -8,5 +9,6 @@ SRC +=    src/aig/ntl/ntlCheck.c \
     src/aig/ntl/ntlReadBlif.c \
     src/aig/ntl/ntlTable.c \
     src/aig/ntl/ntlTime.c \
+    src/aig/ntl/ntlUtil.c \
     src/aig/ntl/ntlWriteBlif.c
 
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index 6d4f5c29..2e109f05 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -103,9 +103,8 @@ struct Ntl_Obj_t_
     Ntl_Mod_t *        pModel;         // the model  
     void *             pCopy;          // the copy of this object
     unsigned           Type   :  3;    // object type
-    unsigned           Id     : 27;    // object ID
-    unsigned           MarkA  :  1;    // temporary mark  
-    unsigned           MarkB  :  1;    // temporary mark
+    unsigned           fMark  :  1;    // temporary mark  
+    unsigned           Id     : 28;    // object ID
     int                nFanins;        // the number of fanins
     int                nFanouts;       // the number of fanouts
     union {                            // functionality
@@ -123,6 +122,7 @@ struct Ntl_Net_t_
     Ntl_Obj_t *        pDriver;        // driver of the net
     char               nVisits;        // the number of times the net is visited
     char               fMark;          // temporary mark
+    char               fCompl;         // complemented attribue
     char               pName[0];       // the name of this net
 };
 
@@ -234,6 +234,7 @@ extern Aig_Man_t *     Ntl_ManCollapse( Ntl_Man_t * p );
 extern char *          Ntl_SopFromTruth( Ntl_Man_t * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover );
 /*=== ntlInsert.c ==========================================================*/
 extern int             Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
+extern int             Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig );
 extern int             Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk );
 /*=== ntlCheck.c ==========================================================*/
 extern int             Ntl_ManCheck( Ntl_Man_t * pMan );
@@ -270,12 +271,17 @@ extern Ntl_Net_t *     Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
 extern Ntl_Net_t *     Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
 extern int             Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber );
 extern int             Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
+extern void            Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet );
 /*=== ntlTime.c ==========================================================*/
 extern Tim_Man_t *     Ntl_ManCreateTiming( Ntl_Man_t * p );
 /*=== ntlReadBlif.c ==========================================================*/
 extern Ntl_Man_t *     Ioa_ReadBlif( char * pFileName, int fCheck );
 /*=== ntlWriteBlif.c ==========================================================*/
 extern void            Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName );
+/*=== ntlUtil.c ==========================================================*/
+extern int             Ntl_ManTransformCoDrivers( Ntl_Man_t * p );
+extern Vec_Ptr_t *     Ntl_ManCollectCiNames( Ntl_Man_t * p );
+extern Vec_Ptr_t *     Ntl_ManCollectCoNames( Ntl_Man_t * p );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index cd21c95f..848f113a 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -213,6 +213,41 @@ char * Ntl_SopCreateFromIsop( Aig_MmFlex_t * pMan, int nVars, Vec_Int_t * vCover
 
 /**Function*************************************************************
 
+  Synopsis    [Creates the cover from the ISOP computed from TT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_SopToIsop( char * pSop, Vec_Int_t * vCover )
+{
+    char * pCube;
+    int k, nVars, Entry;
+    nVars = Ntl_SopGetVarNum( pSop );
+    assert( nVars > 0 );
+    // create cubes
+    Vec_IntClear( vCover );
+    for ( pCube = pSop; *pCube; pCube += nVars + 3 )
+    {
+        Entry = 0;
+        for ( k = nVars - 1; k >= 0; k-- )
+            if ( pCube[k] == '0' )
+                Entry = (Entry << 2) | 1;
+            else if ( pCube[k] == '1' )
+                Entry = (Entry << 2) | 2;
+            else if ( pCube[k] == '-' )
+                Entry = (Entry << 2);
+            else 
+                assert( 0 );
+        Vec_IntPush( vCover, Entry );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Transforms truth table into the SOP.]
 
   Description []
@@ -404,10 +439,11 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
         }
 //printf( "Creating fake PO with ID = %d.\n", Aig_ManPo(p->pAig, Vec_IntEntryLast(p->vBox1Cos))->Id );
     }
-    // store the node
     Vec_PtrPush( p->vNodes, pObj );
     if ( Ntl_ObjIsNode(pObj) )
         pNet->pCopy = Ntl_ManBuildNodeAig( pObj );
+    if ( pNet->fCompl )
+        pNet->pCopy = Aig_Not(pNet->pCopy);
     pNet->nVisits = 2;
     return 1;
 }
@@ -602,9 +638,10 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
         if ( !Ntl_ManBuildModelAig( p, pObj ) )
             return 0;
     }
-    // store the node
     if ( Ntl_ObjIsNode(pObj) )
         pNet->pCopy = Ntl_ManBuildNodeAig( pObj );
+    if ( pNet->fCompl )
+        pNet->pCopy = Aig_Not(pNet->pCopy);
     pNet->nVisits = 2;
     return 1;
 }
@@ -692,6 +729,174 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
     return pAig;    
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Increments reference counter of the net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Ntl_NetIncrementRefs( Ntl_Net_t * pNet )
+{
+    int nRefs = (int)pNet->pCopy;
+    pNet->pCopy = (void *)(nRefs + 1);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts logic newtork out of the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Obj_t * Ntl_ManExtractNwk_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, Nwk_Man_t * pNtk, Vec_Int_t * vCover, Vec_Int_t * vMemory )
+{
+    extern Hop_Obj_t * Kit_CoverToHop( Hop_Man_t * pMan, Vec_Int_t * vCover, int nVars, Vec_Int_t * vMemory );
+    Ntl_Net_t * pFaninNet;
+    Nwk_Obj_t * pNode;
+    int i;
+    if ( pNet->fMark )
+        return pNet->pCopy;
+    pNet->fMark = 1;
+    pNode = Nwk_ManCreateNode( pNtk, Ntl_ObjFaninNum(pNet->pDriver), (int)pNet->pCopy );
+    Ntl_ObjForEachFanin( pNet->pDriver, pFaninNet, i )
+    {
+        Ntl_ManExtractNwk_rec( p, pFaninNet, pNtk, vCover, vMemory );
+        Nwk_ObjAddFanin( pNode, pFaninNet->pCopy );
+    }
+    if ( Ntl_ObjFaninNum(pNet->pDriver) == 0 )
+        pNode->pFunc = Hop_NotCond( Hop_ManConst1(pNtk->pManHop), Ntl_SopIsConst0(pNet->pDriver->pSop) );
+    else
+    {
+        Ntl_SopToIsop( pNet->pDriver->pSop, vCover );
+        pNode->pFunc = Kit_CoverToHop( pNtk->pManHop, vCover, Ntl_ObjFaninNum(pNet->pDriver), vMemory );
+    }
+    return pNet->pCopy = pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts logic newtork out of the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig )
+{
+    Nwk_Man_t * pNtk;
+    Nwk_Obj_t * pNode;
+    Ntl_Mod_t * pRoot;
+    Ntl_Net_t * pNet;
+    Ntl_Obj_t * pObj;
+    Aig_Obj_t * pAnd;
+    Vec_Int_t * vCover, * vMemory;
+    int i, k;
+    pRoot = Ntl_ManRootModel( p );
+    assert( Ntl_ModelBoxNum(pRoot) == 0 );
+    assert( Ntl_ModelLatchNum(pRoot) == 0 );
+    assert( Ntl_ModelPiNum(pRoot) == Aig_ManPiNum(pAig) );
+    assert( Ntl_ModelPoNum(pRoot) == Aig_ManPoNum(pAig) );
+    vCover = Vec_IntAlloc( 100 );
+    vMemory = Vec_IntAlloc( 1 << 16 );
+    // count the number of fanouts of each net
+    Ntl_ModelForEachNet( pRoot, pNet, i )
+    {
+        pNet->pCopy = NULL;
+        pNet->fMark = 0;
+    }
+    Ntl_ModelForEachObj( pRoot, pObj, i )
+        Ntl_ObjForEachFanin( pObj, pNet, k )
+            Ntl_NetIncrementRefs( pNet );
+    // construct the network
+    pNtk = Nwk_ManAlloc();
+    pNtk->pName = Aig_UtilStrsav( pAig->pName );
+    pNtk->pSpec = Aig_UtilStrsav( pAig->pSpec );
+    Aig_ManSetPioNumbers( pAig );
+    Aig_ManForEachObj( pAig, pAnd, i )
+    {
+        if ( Aig_ObjIsPi(pAnd) )
+        {
+            pObj = Ntl_ModelPi( pRoot, Aig_ObjPioNum(pAnd) );
+            pNet = Ntl_ObjFanout0(pObj);
+            pNet->fMark = 1;
+            pNet->pCopy = Nwk_ManCreateCi( pNtk, (int)pNet->pCopy ); 
+        }
+        else if ( Aig_ObjIsPo(pAnd) )
+        {
+            pObj = Ntl_ModelPo( pRoot, Aig_ObjPioNum(pAnd) );
+            pNet = Ntl_ObjFanin0(pObj);
+            pNet->pCopy = Ntl_ManExtractNwk_rec( p, pNet, pNtk, vCover, vMemory ); 
+            pNode = Nwk_ManCreateCo( pNtk );
+            pNode->fCompl = pNet->fCompl;
+            Nwk_ObjAddFanin( pNode, pNet->pCopy );
+        }
+    }
+    Aig_ManCleanPioNumbers( pAig );
+    Ntl_ModelForEachNet( pRoot, pNet, i )
+    {
+        pNet->pCopy = NULL;
+        pNet->fMark = 0;
+    }
+    Vec_IntFree( vCover );
+    Vec_IntFree( vMemory );
+    // create timing manager from the current design
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts logic newtork out of the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Man_t * Ntl_ManReadNwk( char * pFileName, Aig_Man_t * pAig, Tim_Man_t * pManTime )
+{
+    Nwk_Man_t * pNtk;
+    Ntl_Man_t * pNtl;
+    Ntl_Mod_t * pRoot;
+    pNtl = Ioa_ReadBlif( pFileName, 1 );
+    if ( pNtl == NULL )
+    {
+        printf( "Ntl_ManReadNwk(): Reading BLIF has failed.\n" );
+        return NULL;
+    }
+    pRoot = Ntl_ManRootModel( pNtl );
+    if ( Ntl_ModelPiNum(pRoot) != Aig_ManPiNum(pAig) )
+    {
+        printf( "Ntl_ManReadNwk(): The number of primary inputs does not match (%d and %d).\n",
+            Ntl_ModelPiNum(pRoot), Aig_ManPiNum(pAig) );
+        return NULL;
+    }
+    if ( Ntl_ModelPoNum(pRoot) != Aig_ManPoNum(pAig) )
+    {
+        printf( "Ntl_ManReadNwk(): The number of primary outputs does not match (%d and %d).\n",
+            Ntl_ModelPoNum(pRoot), Aig_ManPoNum(pAig) );
+        return NULL;
+    }
+    pNtk = Ntl_ManExtractNwk( pNtl, pAig );
+    Ntl_ManFree( pNtl );
+    if ( pManTime )
+        pNtk->pManTime = Tim_ManDup( pManTime, 0 );
+    return pNtk;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
new file mode 100644
index 00000000..7153f081
--- /dev/null
+++ b/src/aig/ntl/ntlFraig.c
@@ -0,0 +1,156 @@
+/**CFile****************************************************************
+
+  FileName    [ntlFraig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Performing fraiging with white-boxes.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntlFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns AIG with WB after fraiging.]
+
+  Description [pAig points to the nodes of pNew derived using it.
+  pNew points to the nodes of pAigCol derived using it.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_Man_t * pAigCol )
+{
+    Ntl_Net_t * pNet;
+    Aig_Obj_t ** pReprs = NULL, ** pMapBack = NULL;
+    Aig_Obj_t * pObj, * pObjCol, * pObjColRepr, * pCorresp;
+    int i;
+
+    // map the AIG managers
+    Aig_ManForEachObj( pAig, pObj, i )
+        if ( Aig_ObjIsConst1(pObj) )
+            pObj->pData = Aig_ManConst1(pAigCol);
+        else if ( !Aig_ObjIsPo(pObj) )
+        {
+            pNet = pObj->pData;
+            pObjCol = Aig_Regular(pNet->pCopy);
+            pObj->pData = pObjCol;
+        }
+
+    // create mapping from the collapsed manager into the original manager
+    pMapBack = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAigCol) );
+    memset( pMapBack, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAigCol) );
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        if ( Aig_ObjIsPo(pObj) )
+            continue;
+        pObjCol = pObj->pData;
+        if ( pMapBack[pObjCol->Id] == NULL )
+            pMapBack[pObjCol->Id] = pObj;
+    }
+
+    // create the equivalence classes for the original manager
+    pReprs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
+    memset( pReprs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) );
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        if ( Aig_ObjIsPo(pObj) )
+            continue;
+        // get the collapsed node
+        pObjCol = pObj->pData;
+        // get the representative of the collapsed node
+        pObjColRepr = pAigCol->pReprs[pObjCol->Id];
+        if ( pObjColRepr == NULL )
+            pObjColRepr = pObjCol;
+        // get the corresponding original node
+        pCorresp = pMapBack[pObjColRepr->Id];
+        if ( pCorresp == NULL || pCorresp == pObj )
+            continue;
+        // set the representative
+        if ( pCorresp->Id < pObj->Id )
+            pReprs[pObj->Id] = pCorresp;
+        else
+            pReprs[pCorresp->Id] = pObj;
+    }
+    free( pMapBack );
+    return pReprs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns AIG with WB after fraiging.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManFraig( Ntl_Man_t * p, Aig_Man_t * pAig, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose )
+{
+    Ntl_Man_t * pNew;
+    Aig_Man_t * pAigCol, * pTemp;
+    assert( pAig->pReprs == NULL );
+
+    // create a new netlist whose nodes are in 1-to-1 relationship with AIG
+    pNew = Ntl_ManDup( p );
+    if ( !Ntl_ManInsertAig( pNew, pAig ) )
+    {
+        Ntl_ManFree( pNew );
+        printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
+        return NULL;
+    }
+
+    // collapse the AIG
+    pAigCol = Ntl_ManCollapse( pNew );
+    // perform fraiging for the given design
+    if ( nPartSize == 0 )
+        nPartSize = Aig_ManPoNum(pAigCol);
+    pTemp = Aig_ManFraigPartitioned( pAigCol, nPartSize, nConfLimit, nLevelMax, fVerbose );
+    Aig_ManStop( pTemp );
+
+    // transfer equivalence classes to the original AIG
+    pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
+    pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
+    // cleanup
+    Aig_ManStop( pAigCol );
+    Ntl_ManFree( pNew );
+
+    // derive the new AIG
+    pTemp = Aig_ManDupRepresDfs( pAig );
+    // duplicate the timing manager
+    if ( pAig->pManTime )
+        pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 );
+    // reset levels
+    Aig_ManChoiceLevel( pTemp );
+    return pTemp;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c
index f02b4716..10b83660 100644
--- a/src/aig/ntl/ntlInsert.c
+++ b/src/aig/ntl/ntlInsert.c
@@ -59,6 +59,7 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
     pRoot = Ntl_ManRootModel( p );
     Ntl_ModelForEachNode( pRoot, pNode, i )
         Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
+    pRoot->nObjs[NTL_OBJ_NODE] = 0;
     // start mapping of AIG nodes into their copies
     vCopies = Vec_PtrStart( Aig_ManObjNumMax(pAig) );
     Ntl_ManForEachCiNet( p, pNet, i )
@@ -134,6 +135,122 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
   SeeAlso     []
 
 ***********************************************************************/
+int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
+{
+    char Buffer[100];
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pNode;
+    Ntl_Net_t * pNet, * pNetCo;
+    Aig_Obj_t * pObj, * pFanin;
+    int i, nDigits, Counter;
+    assert( Vec_PtrSize(p->vCis) == Aig_ManPiNum(pAig) );
+    assert( Vec_PtrSize(p->vCos) == Aig_ManPoNum(pAig) );
+    // set the correspondence between the PI/PO nodes
+    Aig_ManCleanData( pAig );
+    Ntl_ManForEachCiNet( p, pNet, i )
+        Aig_ManPi( pAig, i )->pData = pNet;
+//    Ntl_ManForEachCoNet( p, pNet, i )
+//        Nwk_ManCo( pNtk, i )->pCopy = pNet;
+    // remove old nodes
+    pRoot = Ntl_ManRootModel( p );
+    Ntl_ModelForEachNode( pRoot, pNode, i )
+        Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
+    pRoot->nObjs[NTL_OBJ_NODE] = 0;
+    // create constant node if needed
+    if ( Aig_ManConst1(pAig)->nRefs > 0 )
+    {
+        pNode = Ntl_ModelCreateNode( pRoot, 0 );
+        pNode->pSop = Ntl_ManStoreSop( p, " 1\n" );
+        if ( (pNet = Ntl_ModelFindNet( pRoot, "Const1" )) )
+        {
+            printf( "Ntl_ManInsertAig(): Internal error: Intermediate net name is not unique.\n" );
+            return 0;
+        }
+        pNet = Ntl_ModelFindOrCreateNet( pRoot, "Const1" );
+        if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
+        {
+            printf( "Ntl_ManInsertAig(): Internal error: Net has more than one fanin.\n" );
+            return 0;
+        }
+        Aig_ManConst1(pAig)->pData = pNet;
+    }
+    // create a new node for each LUT
+    Counter = 0;
+    nDigits = Aig_Base10Log( Aig_ManNodeNum(pAig) );
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        if ( !Aig_ObjIsNode(pObj) )
+            continue;
+        if ( Aig_ObjFanin0(pObj)->pData == NULL || Aig_ObjFanin1(pObj)->pData == NULL )
+        {
+            printf( "Ntl_ManInsertAig(): Internal error: Net not found.\n" );
+            return 0;
+        }
+        pNode = Ntl_ModelCreateNode( pRoot, 2 );
+        Ntl_ObjSetFanin( pNode, Aig_ObjFanin0(pObj)->pData, 0 );
+        Ntl_ObjSetFanin( pNode, Aig_ObjFanin1(pObj)->pData, 1 );
+        if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
+            pNode->pSop = Ntl_ManStoreSop( p, "00 1\n" );
+        else if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) )
+            pNode->pSop = Ntl_ManStoreSop( p, "01 1\n" );
+        else if ( !Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
+            pNode->pSop = Ntl_ManStoreSop( p, "10 1\n" );
+        else // if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
+            pNode->pSop = Ntl_ManStoreSop( p, "11 1\n" );
+        sprintf( Buffer, "and%0*d", nDigits, Counter++ );
+        if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
+        {
+            printf( "Ntl_ManInsertAig(): Internal error: Intermediate net name is not unique.\n" );
+            return 0;
+        }
+        pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer );
+        if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
+        {
+            printf( "Ntl_ManInsertAig(): Internal error: Net has more than one fanin.\n" );
+            return 0;
+        }
+        pObj->pData = pNet;
+    }
+    // mark CIs and outputs of the registers
+    Ntl_ManForEachCiNet( p, pNetCo, i )
+        pNetCo->nVisits = 101;
+    // update the CO pointers
+    Ntl_ManForEachCoNet( p, pNetCo, i )
+    {
+        if ( pNetCo->nVisits == 101 )
+            continue;
+        pNetCo->nVisits = 101;
+        // get the corresponding PO and its driver
+        pObj = Aig_ManPo( pAig, i );
+        pFanin = Aig_ObjFanin0( pObj );
+        // get the net driving the driver
+        pNet = pFanin->pData; 
+        pNode = Ntl_ModelCreateNode( pRoot, 1 );
+        pNode->pSop = Aig_ObjFaninC0(pObj)? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
+        Ntl_ObjSetFanin( pNode, pNet, 0 );
+        // update the CO driver net
+        pNetCo->pDriver = NULL;
+        if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
+        {
+            printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
+            return 0;
+        }
+    }
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the given mapping into the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
 {
     char Buffer[100];
@@ -157,6 +274,7 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
     pRoot = Ntl_ManRootModel( p );
     Ntl_ModelForEachNode( pRoot, pNode, i )
         Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
+    pRoot->nObjs[NTL_OBJ_NODE] = 0;
     // create a new node for each LUT
     vTruth = Vec_IntAlloc( 1 << 16 );
     vCover = Vec_IntAlloc( 1 << 16 );
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index 82660263..83219df7 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -267,6 +267,9 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
         if ( Ntl_ObjIsNode(pObj) )
             ((Ntl_Obj_t *)pObj->pCopy)->pSop = Ntl_ManStoreSop( pManNew, pObj->pSop );
     }
+    pModelNew->vDelays = pModelOld->vDelays? Vec_IntDup( pModelOld->vDelays ) : NULL;
+    pModelNew->vArrivals = pModelOld->vArrivals? Vec_IntDup( pModelOld->vArrivals ) : NULL;
+    pModelNew->vRequireds = pModelOld->vRequireds? Vec_IntDup( pModelOld->vRequireds ) : NULL;
     return pModelNew;
 }
 
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index 2cf3caaa..ce3a2051 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -109,6 +109,7 @@ Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck )
     FILE * pFile;
     Ioa_ReadMan_t * p;
     Ntl_Man_t * pDesign;
+    int nNodes;
 
     // check that the file is available
     pFile = fopen( pFileName, "rb" );
@@ -164,6 +165,9 @@ Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck )
         }
 
     }
+    // transform the design by removing the CO drivers
+    if ( (nNodes = Ntl_ManTransformCoDrivers(pDesign)) )
+        printf( "The design was transformed by removing %d buf/inv CO drivers.\n", nNodes );
 //Ioa_WriteBlif( pDesign, "_temp_.blif" );
     return pDesign;
 }
@@ -614,6 +618,11 @@ static Ntl_Man_t * Ioa_ReadParse( Ioa_ReadMan_t * p )
         // finalize the network
         Ntl_ModelFixNonDrivenNets( pMod->pNtk );
     }
+    if ( i == 0 )
+        return NULL;
+    // update the design name
+    pMod = Vec_PtrEntry( p->vModels, 0 );
+    p->pDesign->pName = Ntl_ManStoreName( p->pDesign, pMod->pNtk->pName );
     // return the network
     pDesign = p->pDesign;
     p->pDesign = NULL;
diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c
index 909a64fd..df982481 100644
--- a/src/aig/ntl/ntlTable.c
+++ b/src/aig/ntl/ntlTable.c
@@ -134,6 +134,35 @@ Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName )
   SeeAlso     []
 
 ***********************************************************************/
+void Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet )
+{
+    Ntl_Net_t * pEnt, * pPrev;
+    unsigned Key = Ntl_HashString( pNet->pName, p->nTableSize );
+    for ( pPrev = NULL, pEnt = p->pTable[Key]; pEnt; pPrev = pEnt, pEnt = pEnt->pNext )
+        if ( pEnt == pNet )
+            break;
+    if ( pEnt == NULL )
+    {
+        printf( "Ntl_ModelDeleteNet(): Net to be deleted is not found in the hash table.\n" );
+        return;
+    }
+    if ( pPrev == NULL )
+        p->pTable[Key] = pEnt->pNext;
+    else
+        pPrev->pNext = pEnt->pNext;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds or creates the net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName )
 {
     Ntl_Net_t * pEnt;
diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c
new file mode 100644
index 00000000..b13dd3a7
--- /dev/null
+++ b/src/aig/ntl/ntlUtil.c
@@ -0,0 +1,165 @@
+/**CFile****************************************************************
+
+  FileName    [ntlUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Various utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntlUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if netlist was written by ABC with added bufs/invs.]
+
+  Description [Should be called immediately after reading from file.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManTransformCoDrivers( Ntl_Man_t * p )
+{
+    Vec_Ptr_t * vCoNets;
+    Ntl_Net_t * pNetCo, * pNetFanin;
+    Ntl_Obj_t * pObj;
+    Ntl_Mod_t * pRoot;
+    int i, k, Counter;
+    pRoot = Ntl_ManRootModel( p );
+    // collect the nets of the root model
+    vCoNets = Vec_PtrAlloc( 1000 );
+    Ntl_ModelForEachPo( pRoot, pObj, i )
+        if ( !Ntl_ObjFanin0(pObj)->fMark )
+        {
+            Ntl_ObjFanin0(pObj)->fMark = 1;
+            Vec_PtrPush( vCoNets, Ntl_ObjFanin0(pObj) );
+        }
+    Ntl_ModelForEachLatch( pRoot, pObj, i )
+        if ( !Ntl_ObjFanin0(pObj)->fMark )
+        {
+            Ntl_ObjFanin0(pObj)->fMark = 1;
+            Vec_PtrPush( vCoNets, Ntl_ObjFanin0(pObj) );
+        }
+    Ntl_ModelForEachBox( pRoot, pObj, k )
+    Ntl_ObjForEachFanin( pObj, pNetCo, i )
+        if ( !pNetCo->fMark )
+        {
+            pNetCo->fMark = 1;
+            Vec_PtrPush( vCoNets, pNetCo );
+        }
+    // check the nets
+    Vec_PtrForEachEntry( vCoNets, pNetCo, i )
+    {
+        if ( !Ntl_ObjIsNode(pNetCo->pDriver) )
+            continue;
+        if ( Ntl_ObjFaninNum(pNetCo->pDriver) != 1 )
+            break;
+        pNetFanin = Ntl_ObjFanin0(pNetCo->pDriver);
+        if ( !Ntl_ObjIsNode(pNetFanin->pDriver) )
+            break;
+    }
+    if ( i < Vec_PtrSize(vCoNets) )
+    {
+        Vec_PtrFree( vCoNets );
+        return 0;
+    }
+
+
+    // remove the buffers/inverters
+    Counter = 0;
+    Vec_PtrForEachEntry( vCoNets, pNetCo, i )
+    {
+        pNetCo->fMark = 0;
+        if ( !Ntl_ObjIsNode(pNetCo->pDriver) )
+            continue;
+        // if this net is driven by an interver
+        // set the complemented attribute of the CO
+        assert( Ntl_ObjFaninNum(pNetCo->pDriver) == 1 );
+        pNetCo->fCompl = (int)(pNetCo->pDriver->pSop[0] == '0');
+        // remove the driver
+        Vec_PtrWriteEntry( pRoot->vObjs, pNetCo->pDriver->Id, NULL );
+        // remove the net
+        pNetFanin = Ntl_ObjFanin0(pNetCo->pDriver);
+        Ntl_ModelDeleteNet( pRoot, pNetFanin );
+        // make the CO net point to the new driver
+        assert( Ntl_ObjIsNode(pNetFanin->pDriver) );
+        pNetCo->pDriver = NULL;
+        pNetFanin->pDriver->pFanio[pNetFanin->pDriver->nFanins] = NULL;
+        Ntl_ModelSetNetDriver( pNetFanin->pDriver, pNetCo );
+        Counter++;
+    }
+    Vec_PtrFree( vCoNets );
+    pRoot->nObjs[NTL_OBJ_NODE] -= Counter;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the array of CI names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ntl_ManCollectCiNames( Ntl_Man_t * p )
+{
+    Vec_Ptr_t * vNames;
+    Ntl_Net_t * pNet;
+    int i;
+    vNames = Vec_PtrAlloc( 1000 );
+    Ntl_ManForEachCiNet( p, pNet, i )
+        Vec_PtrPush( vNames, pNet->pName );
+    return vNames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the array of CI names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ntl_ManCollectCoNames( Ntl_Man_t * p )
+{
+    Vec_Ptr_t * vNames;
+    Ntl_Net_t * pNet;
+    int i;
+    vNames = Vec_PtrAlloc( 1000 );
+    Ntl_ManForEachCoNet( p, pNet, i )
+        Vec_PtrPush( vNames, pNet->pName );
+    return vNames;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c
index 8bcd2044..fddd4167 100644
--- a/src/aig/ntl/ntlWriteBlif.c
+++ b/src/aig/ntl/ntlWriteBlif.c
@@ -44,6 +44,7 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
 {
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
+    float Delay;
     int i, k;
     fprintf( pFile, ".model %s\n", pModel->pName );
     fprintf( pFile, ".inputs" );
@@ -54,6 +55,51 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
     Ntl_ModelForEachPo( pModel, pObj, i )
         fprintf( pFile, " %s", Ntl_ObjFanin0(pObj)->pName );
     fprintf( pFile, "\n" );
+    // write delays
+    if ( pModel->vDelays )
+    {
+        for ( i = 0; i < Vec_IntSize(pModel->vDelays); i += 3 )
+        {
+            fprintf( pFile, ".delay" );
+            fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vDelays,i)))->pName );
+            fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vDelays,i+1)))->pName );
+            fprintf( pFile, " %.3f", Aig_Int2Float(Vec_IntEntry(pModel->vDelays,i+2)) );
+            fprintf( pFile, "\n" );
+        }
+    }
+    if ( pModel->vArrivals )
+    {
+        for ( i = 0; i < Vec_IntSize(pModel->vArrivals); i += 2 )
+        {
+            fprintf( pFile, ".input_arrival" );
+            fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vArrivals,i)))->pName );
+            Delay = Aig_Int2Float(Vec_IntEntry(pModel->vArrivals,i+1));
+            if ( Delay == -TIM_ETERNITY )
+                fprintf( pFile, " -inf" );
+            else if ( Delay == TIM_ETERNITY )
+                fprintf( pFile, " inf" );
+            else
+                fprintf( pFile, " %.3f", Delay );
+            fprintf( pFile, "\n" );
+        }
+    }
+    if ( pModel->vRequireds )
+    {
+        for ( i = 0; i < Vec_IntSize(pModel->vRequireds); i += 2 )
+        {
+            fprintf( pFile, ".output_required" );
+            fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vRequireds,i)))->pName );
+            Delay = Aig_Int2Float(Vec_IntEntry(pModel->vRequireds,i+1));
+            if ( Delay == -TIM_ETERNITY )
+                fprintf( pFile, " -inf" );
+            else if ( Delay == TIM_ETERNITY )
+                fprintf( pFile, " inf" );
+            else
+                fprintf( pFile, " %.3f", Delay );
+            fprintf( pFile, "\n" );
+        }
+    }
+    // write objects
     Ntl_ModelForEachObj( pModel, pObj, i )
     {
         if ( Ntl_ObjIsNode(pObj) )
diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h
index eafc1bbf..4c99c3a9 100644
--- a/src/aig/nwk/nwk.h
+++ b/src/aig/nwk/nwk.h
@@ -252,6 +252,7 @@ extern int             Nwk_ManGetAigNodeNum( Nwk_Man_t * pNtk );
 extern int             Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
 extern int             Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
 extern void            Nwk_ObjPrint( Nwk_Obj_t * pObj );
+extern void            Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/nwk/nwkMan.c b/src/aig/nwk/nwkMan.c
index 2d0254f2..9c2c5ed8 100644
--- a/src/aig/nwk/nwkMan.c
+++ b/src/aig/nwk/nwkMan.c
@@ -91,6 +91,29 @@ void Nwk_ManFree( Nwk_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Nwk_ManPrintLutSizes( Nwk_Man_t * p, If_Lib_t * pLutLib )
+{
+    Nwk_Obj_t * pObj;
+    int i, Counters[256] = {0};
+    Nwk_ManForEachNode( p, pObj, i )
+        Counters[Nwk_ObjFaninNum(pObj)]++;
+    printf( "LUTs by size: " );
+    for ( i = 0; i <= pLutLib->LutMax; i++ )
+        printf( "%d:%d ", i, Counters[i] );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints stats of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib )
 {
     p->pLutLib = pLutLib;
@@ -104,7 +127,8 @@ void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib )
     printf( "aig = %6d  ",   Nwk_ManGetAigNodeNum(p) );
     printf( "lev = %3d  ",   Nwk_ManLevel(p) );
 //    printf( "lev2 = %3d  ",  Nwk_ManLevelBackup(p) );
-    printf( "delay = %5.2f", Nwk_ManDelayTraceLut(p) );
+    printf( "delay = %5.2f   ", Nwk_ManDelayTraceLut(p) );
+    Nwk_ManPrintLutSizes( p, pLutLib );
     printf( "\n" );
 //    Nwk_ManDelayTracePrint( p, pLutLib );
     fflush( stdout );
diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c
index acbfbc0a..6c1e1330 100644
--- a/src/aig/nwk/nwkMap.c
+++ b/src/aig/nwk/nwkMap.c
@@ -134,7 +134,7 @@ If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
         if ( Aig_ObjIsChoice( p, pNode ) )
         {
             pIfMan->nChoices++;
-            for ( pPrev = pNode, pFanin = p->pEquivs[pNode->Id]; pFanin; pPrev = pFanin, pFanin = p->pEquivs[pFanin->Id] )
+            for ( pPrev = pNode, pFanin = Aig_ObjEquiv(p, pNode); pFanin; pPrev = pFanin, pFanin = Aig_ObjEquiv(p, pFanin) )
                 If_ObjSetChoice( pPrev->pData, pFanin->pData );
             If_ManCreateChoice( pIfMan, pNode->pData );
         }
diff --git a/src/aig/nwk/nwkSpeedup.c b/src/aig/nwk/nwkSpeedup.c
index 80404a44..b7802f72 100644
--- a/src/aig/nwk/nwkSpeedup.c
+++ b/src/aig/nwk/nwkSpeedup.c
@@ -137,7 +137,7 @@ void Aig_ManSpeedupNode( Nwk_Man_t * pNtk, Aig_Man_t * pAig, Nwk_Obj_t * pNode,
     // create choice node
     pAnd  = Aig_Regular(pNode->pCopy); // repr
     pTemp = Aig_Regular(ppCofs[0]);    // new
-    if ( pAig->pEquivs[pAnd->Id] == NULL && pAig->pEquivs[pTemp->Id] == NULL && !Aig_ObjCheckTfi(pAig, pTemp, pAnd) )
+    if ( Aig_ObjEquiv(pAig, pAnd) == NULL && Aig_ObjEquiv(pAig, pTemp) == NULL && !Aig_ObjCheckTfi(pAig, pTemp, pAnd) )
         pAig->pEquivs[pAnd->Id] = pTemp;
 }
 
@@ -339,9 +339,9 @@ Aig_Man_t * Nwk_ManSpeedup( Nwk_Man_t * pNtk, int fUseLutLib, int Percentage, in
 
     // remove invalid choice nodes
     Aig_ManForEachNode( pAig, pAnd, i )
-        if ( pAig->pEquivs[pAnd->Id] )
+        if ( Aig_ObjEquiv(pAig, pAnd) )
         {
-            if ( Aig_ObjRefs(pAig->pEquivs[pAnd->Id]) > 0 )
+            if ( Aig_ObjRefs(Aig_ObjEquiv(pAig, pAnd)) > 0 )
                 pAig->pEquivs[pAnd->Id] = NULL;
         }
 
diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c
index b25fd68a..5fb594ec 100644
--- a/src/aig/nwk/nwkUtil.c
+++ b/src/aig/nwk/nwkUtil.c
@@ -238,6 +238,21 @@ void Nwk_ObjPrint( Nwk_Obj_t * pObj )
     printf( "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames )
+{
+    printf( "Dumping logic network is currently not supported.\n" );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 7a995c71..79bf41a1 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -72,8 +72,8 @@ void Abc_ObjRecycle( Abc_Obj_t * pObj )
     Abc_Ntk_t * pNtk = pObj->pNtk;
     int LargePiece = (4 << ABC_NUM_STEPS);
     // free large fanout arrays
-    if ( pNtk->pMmStep && pObj->vFanouts.nCap * 4 > LargePiece )
-        FREE( pObj->vFanouts.pArray );
+//    if ( pNtk->pMmStep && pObj->vFanouts.nCap * 4 > LargePiece )
+//        FREE( pObj->vFanouts.pArray );
     if ( pNtk->pMmStep == NULL )
     {
         FREE( pObj->vFanouts.pArray );
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index dc3595c1..b2d6b649 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -439,6 +439,41 @@ char * Abc_SopCreateFromIsop( Extra_MmFlex_t * pMan, int nVars, Vec_Int_t * vCov
 
 /**Function*************************************************************
 
+  Synopsis    [Creates the cover from the ISOP computed from TT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_SopToIsop( char * pSop, Vec_Int_t * vCover )
+{
+    char * pCube;
+    int k, nVars, Entry;
+    nVars = Abc_SopGetVarNum( pSop );
+    assert( nVars > 0 );
+    // create cubes
+    Vec_IntClear( vCover );
+    for ( pCube = pSop; *pCube; pCube += nVars + 3 )
+    {
+        Entry = 0;
+        for ( k = nVars - 1; k >= 0; k-- )
+            if ( pCube[k] == '0' )
+                Entry = (Entry << 2) | 1;
+            else if ( pCube[k] == '1' )
+                Entry = (Entry << 2) | 2;
+            else if ( pCube[k] == '-' )
+                Entry = (Entry << 2);
+            else 
+                assert( 0 );
+        Vec_IntPush( vCover, Entry );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reads the number of cubes in the cover.]
 
   Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index fb0a6bd6..11d0aec8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -202,7 +202,9 @@ static int Abc_CommandTraceStart     ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandTraceCheck     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandAbc8Read       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8ReadLogic  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Write      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8WriteLogic ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Ps         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8If         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8DChoice    ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -438,7 +440,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "enlarge",       Abc_CommandEnlarge,          1 );
 
     Cmd_CommandAdd( pAbc, "ABC8",         "*r",            Abc_CommandAbc8Read,         0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*rlogic",       Abc_CommandAbc8ReadLogic,    0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*w",            Abc_CommandAbc8Write,        0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*wlogic",       Abc_CommandAbc8WriteLogic,   0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*ps",           Abc_CommandAbc8Ps,           0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*if",           Abc_CommandAbc8If,           0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*dchoice",      Abc_CommandAbc8DChoice,      0 );
@@ -457,7 +461,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC8",         "*lcorr",        Abc_CommandAbc8Lcorr,        0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*ssw",          Abc_CommandAbc8Ssw,          0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*dsec",         Abc_CommandAbc8DSec,         0 );
-
+ 
 
 //    Cmd_CommandAdd( pAbc, "Verification", "trace_start",   Abc_CommandTraceStart,       0 );
 //    Cmd_CommandAdd( pAbc, "Verification", "trace_check",   Abc_CommandTraceCheck,       0 );
@@ -11007,7 +11011,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->fFancy      =  0;
     pPars->fExpRed     =  1;
     pPars->fLatchPaths =  0;
-    pPars->fEdge       =  0;
+    pPars->fEdge       =  1;
     pPars->fCutMin     =  0;
     pPars->fSeqMap     =  0;
     pPars->fBidec      =  0;
@@ -14784,22 +14788,100 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc8ReadLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pFile;
+    char * pFileName;
+    void * pNtkNew;
+    int c;
+    extern void * Ntl_ManReadNwk( char * pFileName, Aig_Man_t * pAig, Tim_Man_t * pManTime );
+    extern Tim_Man_t * Ntl_ManReadTimeMan( void * p );
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    // get the input file name
+    pFileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( pFileName, "r" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open input file \"%s\". ", pFileName );
+        if ( pFileName = Extra_FileGetSimilarName( pFileName, ".blif", NULL, NULL, NULL, NULL ) )
+            fprintf( stdout, "Did you mean \"%s\"?", pFileName );
+        fprintf( stdout, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+
+    if ( pAbc->pAbc8Ntl == NULL || pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8ReadLogic(): There is no design or its AIG.\n" );
+        return 1;
+    }
+
+    // read the new logic
+    pNtkNew = Ntl_ManReadNwk( pFileName, pAbc->pAbc8Aig, Ntl_ManReadTimeMan(pAbc->pAbc8Ntl) );
+    if ( pNtkNew == NULL )
+    {
+        printf( "Abc_CommandAbc8ReadLogic(): Procedure has failed.\n" );
+        return 1;
+    }
+    if ( pAbc->pAbc8Nwk != NULL )
+        Nwk_ManFree( pAbc->pAbc8Nwk );
+    pAbc->pAbc8Nwk = pNtkNew;    
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: *rlogic [-h]\n" );
+    fprintf( stdout, "\t        reads the logic part of the design without whiteboxes\n" );
+    fprintf( stdout, "\t        and sets the new logic as the current mapped network\n" );
+    fprintf( stdout, "\t        (the logic part should be comb and with the same PIs/POs)\n" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     char * pFileName;
     void * pTemp;
+    int fAig;
     int c;
     extern void Ioa_WriteBlif( void * p, char * pFileName );
     extern int Ntl_ManInsertNtk( void * p, void * pNtk );
+    extern int Ntl_ManInsertAig( void * p, Aig_Man_t * pAig );
     extern void * Ntl_ManDup( void * pOld );
     extern void Ntl_ManFree( void * p );
 
     // set defaults
+    fAig = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'a':
+            fAig ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -14813,17 +14895,35 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // create the design to write
     pTemp = Ntl_ManDup( pAbc->pAbc8Ntl );
-    if ( pAbc->pAbc8Nwk != NULL )
+    if ( fAig )
     {
-        if ( !Ntl_ManInsertNtk( pTemp, pAbc->pAbc8Nwk ) )
+        if ( pAbc->pAbc8Aig != NULL )
         {
-            printf( "Abc_CommandAbc8Write(): There is no design to write.\n" );
+            if ( !Ntl_ManInsertAig( pTemp, pAbc->pAbc8Aig ) )
+            {
+                printf( "Abc_CommandAbc8Write(): Inserting AIG has failed.\n" );
+                return 1;
+            }
+        }
+        else
+        {
+            printf( "There is no AIG to write.\n" );
             return 1;
         }
-        printf( "Writing the mapped design.\n" );
     }
-    else
-        printf( "Writing the original design.\n" );
+    else 
+    {
+        if ( pAbc->pAbc8Nwk != NULL ) 
+        {
+            if ( !Ntl_ManInsertNtk( pTemp, pAbc->pAbc8Nwk ) )
+            {
+                printf( "Abc_CommandAbc8Write():  Inserting mapped network has failed.\n" );
+                return 1;
+            }
+        }
+        else
+            printf( "Writing the original design.\n" );
+    }
     // get the input file name
     pFileName = argv[globalUtilOptind];
     Ioa_WriteBlif( pTemp, pFileName );
@@ -14831,8 +14931,87 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: *w [-h]\n" );
+    fprintf( stdout, "usage: *w [-ah]\n" );
     fprintf( stdout, "\t        write the design with whiteboxes\n" );
+    fprintf( stdout, "\t-a    : toggle writing mapped network or AIG [default = %s]\n", fAig? "AIG": "mapped" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8WriteLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Vec_Ptr_t * vCiNames = NULL, * vCoNames = NULL;
+    char * pFileName;
+    int fAig;
+    int c;
+    extern Vec_Ptr_t * Ntl_ManCollectCiNames( void * p );
+    extern Vec_Ptr_t * Ntl_ManCollectCoNames( void * p );
+    extern void Nwk_ManDumpBlif( void * p, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames );
+
+    // set defaults
+    fAig = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'a':
+            fAig ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Write(): There is no design to write.\n" );
+        return 1;
+    }
+    // create the design to write
+    pFileName = argv[globalUtilOptind];
+//    vCiNames = Ntl_ManCollectCiNames( pAbc->pAbc8Ntl );
+//    vCoNames = Ntl_ManCollectCoNames( pAbc->pAbc8Ntl );
+    if ( fAig )
+    {
+        if ( pAbc->pAbc8Aig != NULL )
+            Aig_ManDumpBlif( pAbc->pAbc8Aig, pFileName, vCiNames, vCoNames );
+        else
+        {
+            printf( "There is no AIG to write.\n" );
+            return 1;
+        }
+    }
+    else 
+    {
+        if ( pAbc->pAbc8Nwk != NULL ) 
+            Nwk_ManDumpBlif( pAbc->pAbc8Nwk, pFileName, vCiNames, vCoNames );
+        else
+        {
+            printf( "There is no mapped network to write.\n" );
+            return 1;
+        }
+    }
+    if ( vCiNames )  Vec_PtrFree( vCiNames );
+    if ( vCoNames )  Vec_PtrFree( vCoNames );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: *wlogic [-ah]\n" );
+    fprintf( stdout, "\t        write the logic part of the design without whiteboxes\n" );
+    fprintf( stdout, "\t-a    : toggle writing mapped network or AIG [default = %s]\n", fAig? "AIG": "mapped" );
     fprintf( stdout, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -15768,7 +15947,98 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    Aig_Man_t * pAigNew;
+    int c, fVerbose;
+    int nPartSize;
+    int nConfLimit;
+    int nLevelMax;
+    extern Aig_Man_t * Ntl_ManFraig( void * p, Aig_Man_t * pAig, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose );
+
+    // set defaults
+    nPartSize    = 0;
+    nConfLimit   = 100;   
+    nLevelMax    = 0;
+    fVerbose     = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PCLvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nPartSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nPartSize < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfLimit < 0 ) 
+                goto usage;
+            break;
+         case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nLevelMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLevelMax < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Fraig(): There is no design to SAT sweep.\n" );
+        return 1;
+    }
+    if ( pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8Fraig(): There is no AIG to SAT sweep.\n" );
+        return 1;
+    }
+
+    // get the input file name
+    pAigNew = Ntl_ManFraig( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, nPartSize, nConfLimit, nLevelMax, fVerbose );
+    if ( pAigNew == NULL )
+    {
+        printf( "Abc_CommandAbc8Fraig(): Tranformation of the AIG has failed.\n" );
+        return 1;
+    }
+    if ( pAbc->pAbc8Aig )
+        Aig_ManStop( pAbc->pAbc8Aig );
+    pAbc->pAbc8Aig = pAigNew;
     return 0;
+
+usage:
+    fprintf( stdout, "usage: *fraig [-P num] [-C num] [-L num] [-vh]\n" );
+    fprintf( stdout, "\t         performs SAT sweeping with white-boxes\n" );
+    fprintf( stdout, "\t-P num : partition size (0 = partitioning is not used) [default = %d]\n", nPartSize );
+    fprintf( stdout, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
+    fprintf( stdout, "\t-L num : limit on node level to fraig (0 = fraig all nodes) [default = %d]\n", nLevelMax );
+    fprintf( stdout, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 4f27057b..81260e0e 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -353,7 +353,7 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
-        if ( (pTemp = pMan->pEquivs[pObj->Id]) )
+        if ( (pTemp = Aig_ObjEquiv(pMan, pObj)) )
         {
             Abc_Obj_t * pAbcRepr, * pAbcObj;
             assert( pTemp->pData != NULL );
diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c
index 9cc4e2c6..171cbf0a 100644
--- a/src/base/abci/abcFpga.c
+++ b/src/base/abci/abcFpga.c
@@ -201,7 +201,7 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pNode, * pNodeNew;
-    int i, nDupGates;
+    int i;//, nDupGates;
     // create the new network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
     // make the mapper point to the new network
@@ -229,7 +229,7 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
     if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
         Abc_NtkDeleteObj( pNodeNew );
     // decouple the PO driver nodes to reduce the number of levels
-    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+//    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
 //    if ( nDupGates && Fpga_ManReadVerbose(pMan) )
 //        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
     return pNtkNew;
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 35ec473f..cf6f88ae 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -186,7 +186,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pNode, * pNodeNew;
     Vec_Int_t * vCover;
-    int i, nDupGates;
+    int i;//, nDupGates;
     // create the new network
     if ( pIfMan->pPars->fUseBdds || pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
         pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
@@ -223,7 +223,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     if ( pIfMan->pPars->fUseBdds )
         Abc_NtkBddReorder( pNtkNew, 0 );
     // decouple the PO driver nodes to reduce the number of levels
-    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+//    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
 //    if ( nDupGates && If_ManReadVerbose(pIfMan) )
 //        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
     return pNtkNew;