Version abc80410

29 files changed, 2054 insertions, 144 deletions

diff --git a/abc.dsp b/abc.dsp
index 9034256e..1f82b4e2 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -3066,6 +3066,10 @@ SOURCE=.\src\aig\ntl\ntlCore.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\ntl\ntlEc.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\ntl\ntlExtract.c
 # End Source File
 # Begin Source File
@@ -3094,6 +3098,10 @@ SOURCE=.\src\aig\ntl\ntlReadBlif.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\ntl\ntlSweep.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\ntl\ntlTable.c
 # End Source File
 # Begin Source File
diff --git a/copyright.txt b/copyright.txt
index 121d63e8..f99ef9ad 100644
--- a/copyright.txt
+++ b/copyright.txt
@@ -1,3 +1,8 @@
+ABC: System for Sequential Synthesis and Verification
+
+http://www.eecs.berkeley.edu/~alanmi/abc/
+
+
 Copyright (c) The Regents of the University of California. All rights reserved.
 
 Permission is hereby granted, without written agreement and without license or
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 2231b4e7..88d7aa50 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -140,6 +140,7 @@ struct Aig_Man_t_
     void *           pManCuts;
     Vec_Ptr_t *      vMapped;
     Vec_Int_t *      vFlopNums;      
+    Vec_Int_t *      vFlopReprs;      
     void *           pSeqModel;
     Aig_Man_t *      pManExdc;
     Vec_Ptr_t *      vOnehots;
@@ -314,7 +315,7 @@ static inline void         Aig_ObjClean( Aig_Obj_t * pObj )       { memset( pObj
 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_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_ObjPioNum( Aig_Obj_t * pObj )      { assert( !Aig_ObjIsNode(pObj) ); return (int)(long)pObj->pNext;                                                    }
 static inline int          Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )    
 { 
     if ( Aig_ObjFanin0(pObj) == pFanin ) return 0; 
@@ -461,6 +462,7 @@ extern Aig_Obj_t *     Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t
 extern void            Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes );
 extern int             Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper );
 /*=== aigDup.c ==========================================================*/
+extern Aig_Man_t *     Aig_ManDup( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupOrdered( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupExor( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupDfs( Aig_Man_t * p );
@@ -560,6 +562,7 @@ extern int             Aig_ManSeqCleanup( Aig_Man_t * p );
 extern int             Aig_ManCountMergeRegs( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
 extern void            Aig_ManComputeSccs( Aig_Man_t * p ); 
+extern Aig_Man_t *     Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose );
 /*=== aigShow.c ========================================================*/
 extern void            Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold );
 /*=== aigTable.c ========================================================*/
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 917558c6..9f7d286d 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -449,10 +449,10 @@ int Aig_ManChoiceLevel( Aig_Man_t * p )
             LevelMax = Aig_ObjLevel(pObj);
     }
     Aig_ManCleanPioNumbers( p );
-    Aig_ManForEachNode( p, pObj, i )
-        assert( Aig_ObjLevel(pObj) > 0 );
+//    Aig_ManForEachNode( p, pObj, i )
+//        assert( Aig_ObjLevel(pObj) > 0 );
     return LevelMax;
-}
+} 
 
 //#endif
 
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index fb0a8ba8..b435aade 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -33,6 +33,72 @@
 
   Synopsis    [Duplicates the AIG manager.]
 
+  Description [Orders nodes as follows: PIs, ANDs, POs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDup( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjNew;
+    int i;
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->nRegs = p->nRegs;
+    pNew->nAsserts = p->nAsserts;
+    if ( p->vFlopNums )
+        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        pObjNew = Aig_ObjCreatePi( pNew );
+        pObjNew->pHaig = pObj->pHaig;
+        pObjNew->Level = pObj->Level;
+        pObj->pData = pObjNew;
+    }
+    // duplicate internal nodes
+    Aig_ManForEachObj( p, pObj, i )
+        if ( Aig_ObjIsBuf(pObj) )
+        {
+            pObjNew = Aig_ObjChild0Copy(pObj);
+            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+            pObj->pData = pObjNew;
+        }
+        else if ( Aig_ObjIsNode(pObj) )
+        {
+            pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+            pObj->pData = pObjNew;
+        }
+    // add the POs
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        pObjNew->pHaig = pObj->pHaig;
+        pObj->pData = pObjNew;
+    }
+    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+    // duplicate the timing manager
+    if ( p->pManTime )
+        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDup(): The check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager.]
+
   Description [Assumes topological ordering of the nodes.]
                
   SideEffects []
@@ -543,7 +609,7 @@ Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p )
     }
     // check the new manager
     if ( !Aig_ManCheck(pNew) )
-        printf( "Aig_ManDupReprentative: Check has failed.\n" );
+        printf( "Aig_ManDupRepres: Check has failed.\n" );
     return pNew;
 }
 
@@ -616,7 +682,7 @@ Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p )
     }
     // check the new manager
     if ( !Aig_ManCheck(pNew) )
-        printf( "Aig_ManDupReprentative: Check has failed.\n" );
+        printf( "Aig_ManDupRepresDfs: Check has failed.\n" );
     return pNew;
 }
 
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 58f0d797..4c4b7aad 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -206,6 +206,7 @@ void Aig_ManStop( Aig_Man_t * p )
     if ( p->vLevelR )  Vec_IntFree( p->vLevelR );
     if ( p->vLevels )  Vec_VecFree( p->vLevels );
     if ( p->vFlopNums) Vec_IntFree( p->vFlopNums );
+    if ( p->vFlopReprs)Vec_IntFree( p->vFlopReprs );
     if ( p->pManExdc ) Aig_ManStop( p->pManExdc );
     if ( p->vOnehots ) Vec_VecFree( (Vec_Vec_t *)p->vOnehots );
     FREE( p->pData );
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index d02e3228..a66eb2b8 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -258,6 +258,8 @@ void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew
     Aig_ObjDeref( pFaninOld );
     // update the fanin
     pObj->pFanin0 = pFaninNew;
+    pObj->Level = Aig_ObjLevelNew( pObj );
+    pObj->fPhase = Aig_ObjPhaseReal(pObj->pFanin0);
     // increment ref and add fanout
     if ( p->pFanData )
         Aig_ObjAddFanout( p, Aig_ObjFanin0(pObj), pObj );
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 4eefa283..94a1c844 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -278,6 +278,8 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
     Aig_ManForEachPi( p, pObj, i )
         pObj->pData = Aig_ObjCreatePi(pNew);
+//    Aig_ManForEachPi( p, pObj, i )
+//        pObj->pData = Aig_ObjGetRepr( p, pObj );
     // map the internal nodes
     if ( fOrdered )
     {
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index 92bfcd28..c32f2f4f 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -44,25 +44,52 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
 {
     Aig_Man_t * pNew;
     Aig_Obj_t * pObj, * pObjMapped;
-    int i;
+    int i, nTruePis;
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
     pNew->nRegs = p->nRegs;
     pNew->nAsserts = p->nAsserts;
+    assert( p->vFlopNums == NULL || Vec_IntSize(p->vFlopNums) == p->nRegs );
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+    if ( p->vFlopReprs )
+        pNew->vFlopReprs = Vec_IntDup( p->vFlopReprs );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
     Aig_ManForEachPi( p, pObj, i )
         pObj->pData = Aig_ObjCreatePi(pNew);
     // implement the mapping
+    nTruePis = Aig_ManPiNum(p)-Aig_ManRegNum(p);
+    if ( p->vFlopReprs )
+    {
+        Aig_ManForEachLoSeq( p, pObj, i )
+            pObj->pNext = (Aig_Obj_t *)(long)Vec_IntEntry( p->vFlopNums, i-nTruePis );
+    }
     Aig_ManForEachPi( p, pObj, i )
     {
         pObjMapped = Vec_PtrEntry( vMap, i );
         pObj->pData = Aig_NotCond( Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) );
+        if ( pNew->vFlopReprs && i >= nTruePis && pObj != pObjMapped )
+        {
+            Vec_IntPush( pNew->vFlopReprs, Aig_ObjPioNum(pObj) );
+            if ( Aig_ObjIsConst1( Aig_Regular(pObjMapped) ) )
+                Vec_IntPush( pNew->vFlopReprs, -1 );
+            else
+            {
+                assert( !Aig_IsComplement(pObjMapped) );
+                assert( Aig_ObjIsPi(pObjMapped) );
+                assert( Aig_ObjPioNum(pObj) != Aig_ObjPioNum(pObjMapped) );
+                Vec_IntPush( pNew->vFlopReprs, Aig_ObjPioNum(pObjMapped) );
+            }
+        }
+    }
+    if ( p->vFlopReprs )
+    {
+        Aig_ManForEachLoSeq( p, pObj, i )
+            pObj->pNext = NULL;
     }
     // duplicate internal nodes
     Aig_ManForEachObj( p, pObj, i )
@@ -158,16 +185,15 @@ int Aig_ManSeqCleanup( Aig_Man_t * p )
         if ( p->vFlopNums )
         {
             int nTruePos = Aig_ManPoNum(p)-Aig_ManRegNum(p);
-            // remember numbers of flops in the flops
-            Aig_ManForEachLiSeq( p, pObj, i )
-                pObj->pNext = (Aig_Obj_t *)(long)Vec_IntEntry( p->vFlopNums, i - nTruePos );
-            // reset the flop numbers
-            Vec_PtrForEachEntryStart( vNodes, pObj, i, nTruePos )
-                Vec_IntWriteEntry( p->vFlopNums, i - nTruePos, (int)(long)pObj->pNext );
-            Vec_IntShrink( p->vFlopNums, Vec_PtrSize(vNodes) - nTruePos );
-            // clean the next pointer
-            Aig_ManForEachLiSeq( p, pObj, i )
-                pObj->pNext = NULL;
+            int iNum, k = 0;
+            Aig_ManForEachPo( p, pObj, i )
+                if ( i >= nTruePos && Aig_ObjIsTravIdCurrent(p, pObj) )
+                {
+                    iNum = Vec_IntEntry( p->vFlopNums, i - nTruePos );
+                    Vec_IntWriteEntry( p->vFlopNums, k++, iNum );
+                }
+            assert( k == Vec_PtrSize(vNodes) - nTruePos );
+            Vec_IntShrink( p->vFlopNums, k );
         }
         // collect new CIs/COs
         vCis = Vec_PtrAlloc( Aig_ManPiNum(p) );
@@ -505,6 +531,54 @@ void Aig_ManComputeSccs( Aig_Man_t * p )
     Vec_VecFree( (Vec_Vec_t *)vSupports );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose )
+{
+    Aig_Man_t * pAigInit, * pAigNew;
+    Aig_Obj_t * pFlop1, * pFlop2;
+    int i, Entry1, Entry2, nTruePis;
+    // store the original AIG
+    assert( pAig->vFlopNums == NULL );
+    pAigInit = pAig;
+    pAig = Aig_ManDup( pAig );
+    // create storage for latch numbers
+    pAig->vFlopNums = Vec_IntStartNatural( pAig->nRegs );
+    pAig->vFlopReprs = Vec_IntAlloc( 100 );
+    Aig_ManSeqCleanup( pAig );
+    if ( fLatchConst && pAig->nRegs )
+        pAig = Aig_ManConstReduce( pAig, fVerbose );
+    if ( fLatchEqual && pAig->nRegs )
+        pAig = Aig_ManReduceLaches( pAig, fVerbose );
+    // translate pairs into reprs
+    nTruePis = Aig_ManPiNum(pAigInit)-Aig_ManRegNum(pAigInit);
+    Aig_ManReprStart( pAigInit, Aig_ManObjNumMax(pAigInit) );
+    Vec_IntForEachEntry( pAig->vFlopReprs, Entry1, i )
+    {
+        Entry2 = Vec_IntEntry( pAig->vFlopReprs, ++i ); 
+        pFlop1 = Aig_ManPi( pAigInit, nTruePis + Entry1 );
+        pFlop2 = (Entry2 == -1)? Aig_ManConst1(pAigInit) : Aig_ManPi( pAigInit, nTruePis + Entry2 );
+        assert( pFlop1 != pFlop2 );
+        if ( pFlop1->Id > pFlop2->Id )
+            pAigInit->pReprs[pFlop1->Id] = pFlop2;
+        else
+            pAigInit->pReprs[pFlop2->Id] = pFlop1;
+    }
+    Aig_ManStop( pAig );
+//    Aig_ManSeqCleanup( pAigInit );
+    pAigNew = Aig_ManDupRepr( pAigInit, 0 );
+    Aig_ManSeqCleanup( pAigNew );
+    return pAigNew;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 389c3e2f..012c7651 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -47,13 +47,18 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fFraiging
     Aig_Man_t * pNew, * pTemp;
     int nFrames, RetValue, nIter, clk, clkTotal = clock();
     int fLatchCorr = 0;
+
+    // try the miter before solving
+    RetValue = Fra_FraigMiterStatus( p );
+    if ( RetValue == 0 || RetValue == 1 )
+        goto finish;
+
     // prepare parameters
     memset( pPars, 0, sizeof(Fra_Ssw_t) );
     pPars->fLatchCorr  = fLatchCorr;
     pPars->fVerbose = fVeryVerbose;
 
-    pNew = Aig_ManDupOrdered( p );
-//    pNew = Aig_ManDupDfs( p );
+    pNew = Aig_ManDup( p );
     if ( fVerbose )
     {
         printf( "Original miter:       Latches = %5d. Nodes = %6d.\n", 
@@ -208,6 +213,7 @@ PRT( "Time", clock() - clkTotal );
     // get the miter status
     RetValue = Fra_FraigMiterStatus( pNew );
 
+finish:
     // report the miter
     if ( RetValue == 1 )
     {
diff --git a/src/aig/ioa/ioaWriteAig.c b/src/aig/ioa/ioaWriteAig.c
index 166dca4b..aa731463 100644
--- a/src/aig/ioa/ioaWriteAig.c
+++ b/src/aig/ioa/ioaWriteAig.c
@@ -145,7 +145,7 @@ static void     Ioa_ObjSetAigerNum( Aig_Obj_t * pObj, unsigned Num )  { pObj->iD
   SeeAlso     []
 
 ***********************************************************************/
-int Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x )
+int Ioa_WriteAigerEncode( unsigned char * pBuffer, int Pos, unsigned x )
 {
     unsigned char ch;
     while (x & ~0x7f)
@@ -332,8 +332,8 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int
         uLit0 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) );
         uLit1 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) );
         assert( uLit0 < uLit1 );
-        Pos = Ioa_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit  - uLit1) );
-        Pos = Ioa_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) );
+        Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit  - uLit1 );
+        Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
         if ( Pos > nBufferSize - 10 )
         {
             printf( "Ioa_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
diff --git a/src/aig/ntl/module.make b/src/aig/ntl/module.make
index d3f2cfdd..7f885a90 100644
--- a/src/aig/ntl/module.make
+++ b/src/aig/ntl/module.make
@@ -1,5 +1,6 @@
 SRC +=    src/aig/ntl/ntlCheck.c \
     src/aig/ntl/ntlCore.c \
+    src/aig/ntl/ntlEc.c \
     src/aig/ntl/ntlExtract.c \
     src/aig/ntl/ntlFraig.c \
     src/aig/ntl/ntlInsert.c \
@@ -7,6 +8,7 @@ SRC +=    src/aig/ntl/ntlCheck.c \
     src/aig/ntl/ntlMap.c \
     src/aig/ntl/ntlObj.c \
     src/aig/ntl/ntlReadBlif.c \
+    src/aig/ntl/ntlSweep.c \
     src/aig/ntl/ntlTable.c \
     src/aig/ntl/ntlTime.c \
     src/aig/ntl/ntlUtil.c \
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index 2e109f05..6b6424c0 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -54,8 +54,9 @@ typedef enum {
     NTL_OBJ_PO,                        // 2: primary output
     NTL_OBJ_LATCH,                     // 3: latch node
     NTL_OBJ_NODE,                      // 4: logic node
-    NTL_OBJ_BOX,                       // 5: white box or black box
-    NTL_OBJ_VOID                       // 6: unused object
+    NTL_OBJ_LUT1,                      // 5: inverter/buffer
+    NTL_OBJ_BOX,                       // 6: white box or black box
+    NTL_OBJ_VOID                       // 7: unused object
 } Ntl_Type_t;
 
 struct Ntl_Man_t_
@@ -122,7 +123,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               fCompl;         // complemented attribute
     char               pName[0];       // the name of this net
 };
 
@@ -148,6 +149,7 @@ static inline Ntl_Mod_t * Ntl_ManRootModel( Ntl_Man_t * p )       { return Vec_P
 static inline int         Ntl_ModelPiNum( Ntl_Mod_t * p )         { return p->nObjs[NTL_OBJ_PI];                } 
 static inline int         Ntl_ModelPoNum( Ntl_Mod_t * p )         { return p->nObjs[NTL_OBJ_PO];                } 
 static inline int         Ntl_ModelNodeNum( Ntl_Mod_t * p )       { return p->nObjs[NTL_OBJ_NODE];              } 
+static inline int         Ntl_ModelLut1Num( Ntl_Mod_t * p )       { return p->nObjs[NTL_OBJ_LUT1];              } 
 static inline int         Ntl_ModelLatchNum( Ntl_Mod_t * p )      { return p->nObjs[NTL_OBJ_LATCH];             } 
 static inline int         Ntl_ModelBoxNum( Ntl_Mod_t * p )        { return p->nObjs[NTL_OBJ_BOX];               } 
 static inline int         Ntl_ModelCiNum( Ntl_Mod_t * p )         { return p->nObjs[NTL_OBJ_PI] + p->nObjs[NTL_OBJ_LATCH]; } 
@@ -228,27 +230,35 @@ static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
 /*=== ntlCore.c ==========================================================*/
 extern int             Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig );
 extern int             Ntl_ManInsertTestIf( Ntl_Man_t * p, Aig_Man_t * pAig );
+/*=== ntlEc.c ==========================================================*/
+extern void            Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 );
+extern Aig_Man_t *     Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
 /*=== ntlExtract.c ==========================================================*/
 extern Aig_Man_t *     Ntl_ManExtract( Ntl_Man_t * p );
-extern Aig_Man_t *     Ntl_ManCollapse( Ntl_Man_t * p );
+extern Aig_Man_t *     Ntl_ManCollapse( Ntl_Man_t * p, int fSeq );
+extern Aig_Man_t *     Ntl_ManCollapseForCec( Ntl_Man_t * p );
+extern Aig_Man_t *     Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 );
 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 );
+extern Ntl_Man_t *     Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
+extern Ntl_Man_t *     Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig );
+extern Ntl_Man_t *     Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk );
 /*=== ntlCheck.c ==========================================================*/
 extern int             Ntl_ManCheck( Ntl_Man_t * pMan );
 extern int             Ntl_ModelCheck( Ntl_Mod_t * pModel );
 extern void            Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel );
 /*=== ntlMan.c ============================================================*/
 extern Ntl_Man_t *     Ntl_ManAlloc( char * pFileName );
+extern void            Ntl_ManCleanup( Ntl_Man_t * p );
 extern Ntl_Man_t *     Ntl_ManStartFrom( Ntl_Man_t * p );
 extern Ntl_Man_t *     Ntl_ManDup( Ntl_Man_t * p );
 extern void            Ntl_ManFree( Ntl_Man_t * p );
+extern int             Ntl_ManIsComb( Ntl_Man_t * p );
 extern Ntl_Mod_t *     Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
 extern void            Ntl_ManPrintStats( Ntl_Man_t * p );
 extern Tim_Man_t *     Ntl_ManReadTimeMan( Ntl_Man_t * p );
 extern Ntl_Mod_t *     Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
+extern Ntl_Mod_t *     Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
 extern Ntl_Mod_t *     Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
 extern void            Ntl_ModelFree( Ntl_Mod_t * p );
 /*=== ntlMap.c ============================================================*/
@@ -263,15 +273,19 @@ extern Ntl_Obj_t *     Ntl_ModelCreateLatch( Ntl_Mod_t * pModel );
 extern Ntl_Obj_t *     Ntl_ModelCreateNode( Ntl_Mod_t * pModel, int nFanins );
 extern Ntl_Obj_t *     Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts );
 extern Ntl_Obj_t *     Ntl_ModelDupObj( Ntl_Mod_t * pModel, Ntl_Obj_t * pOld );
+extern Ntl_Obj_t *     Ntl_ModelCreatePiWithName( Ntl_Mod_t * pModel, char * pName );
 extern char *          Ntl_ManStoreName( Ntl_Man_t * p, char * pName );
 extern char *          Ntl_ManStoreSop( Ntl_Man_t * p, char * pSop );
 extern char *          Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName );
+/*=== ntlSweep.c ==========================================================*/
+extern Ntl_Man_t *     Ntl_ManSweep( Ntl_Man_t * p, Aig_Man_t * pAig, int fVerbose );
 /*=== ntlTable.c ==========================================================*/
 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 );
+extern int             Ntl_ModelCountNets( Ntl_Mod_t * p );
 /*=== ntlTime.c ==========================================================*/
 extern Tim_Man_t *     Ntl_ManCreateTiming( Ntl_Man_t * p );
 /*=== ntlReadBlif.c ==========================================================*/
@@ -279,9 +293,15 @@ 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_ModelCountLut1( Ntl_Mod_t * pRoot );
+extern int             Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p );
 extern int             Ntl_ManTransformCoDrivers( Ntl_Man_t * p );
+extern int             Ntl_ManReconnectCoDrivers( Ntl_Man_t * p );
 extern Vec_Ptr_t *     Ntl_ManCollectCiNames( Ntl_Man_t * p );
 extern Vec_Ptr_t *     Ntl_ManCollectCoNames( Ntl_Man_t * p );
+extern void            Ntl_ManMarkCiCoNets( Ntl_Man_t * p );
+extern void            Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p );
+extern int             Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c
index 5973e967..9fd4af9f 100644
--- a/src/aig/ntl/ntlCheck.c
+++ b/src/aig/ntl/ntlCheck.c
@@ -31,7 +31,7 @@
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Checks one model.]
 
   Description []
                
@@ -49,12 +49,12 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel )
     {
         if ( pNet->pName == NULL )
         {
-            printf( "Net %d does not have a name\n", i );
+            printf( "Net in bin %d does not have a name\n", i );
             fStatus = 0;
         }
         if ( pNet->pDriver == NULL )
         {
-            printf( "Net %d (%s) does not have a driver\n", i, pNet->pName );
+            printf( "Net %s does not have a driver\n", pNet->pName );
             fStatus = 0;
         }
     }
@@ -78,7 +78,7 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Checks the netlist.]
 
   Description []
                
@@ -131,7 +131,7 @@ int Ntl_ManCheck( Ntl_Man_t * pMan )
 
 /**Function*************************************************************
 
-  Synopsis    [Reads the verilog file.]
+  Synopsis    [Fixed problems with non-driven nets in the model.]
 
   Description []
                
diff --git a/src/aig/ntl/ntlCore.c b/src/aig/ntl/ntlCore.c
index fb4bb620..a5c40444 100644
--- a/src/aig/ntl/ntlCore.c
+++ b/src/aig/ntl/ntlCore.c
@@ -69,10 +69,13 @@ Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdate
 ***********************************************************************/
 int Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig )
 {
+    Ntl_Man_t * pNew;
     Vec_Ptr_t * vMapping;
     int RetValue;
     vMapping = Ntl_MappingFromAig( pAig );
-    RetValue = Ntl_ManInsert( p, vMapping, pAig );
+    pNew = Ntl_ManInsertMapping( p, vMapping, pAig );
+    RetValue = (pNew != NULL);
+    Ntl_ManFree( pNew );
     Vec_PtrFree( vMapping );
     return RetValue;
 }
@@ -90,10 +93,13 @@ int Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig )
 ***********************************************************************/
 int Ntl_ManInsertTestIf( Ntl_Man_t * p, Aig_Man_t * pAig )
 {
+    Ntl_Man_t * pNew;
     Vec_Ptr_t * vMapping;
     int RetValue;
     vMapping = Ntl_MappingIf( p, pAig );
-    RetValue = Ntl_ManInsert( p, vMapping, pAig );
+    pNew = Ntl_ManInsertMapping( p, vMapping, pAig );
+    RetValue = (pNew != NULL);
+    Ntl_ManFree( pNew );
     Vec_PtrFree( vMapping );
     return RetValue;
 }
diff --git a/src/aig/ntl/ntlEc.c b/src/aig/ntl/ntlEc.c
new file mode 100644
index 00000000..6b7b1a41
--- /dev/null
+++ b/src/aig/ntl/ntlEc.c
@@ -0,0 +1,317 @@
+/**CFile****************************************************************
+
+  FileName    [ntlEc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Equivalence checking procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntlEc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Adds PIs to both models, so that they have the same PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManCreateMissingInputs( Ntl_Mod_t * p1, Ntl_Mod_t * p2, int fSeq )
+{
+    Ntl_Obj_t * pObj;
+    Ntl_Net_t * pNet;
+    int i;
+    Ntl_ModelForEachPi( p1, pObj, i )
+    {
+        pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
+        if ( pNet == NULL )
+            Ntl_ModelCreatePiWithName( p2, Ntl_ObjFanout0(pObj)->pName );
+    }
+    Ntl_ModelForEachPi( p2, pObj, i )
+    {
+        pNet = Ntl_ModelFindNet( p1, Ntl_ObjFanout0(pObj)->pName );
+        if ( pNet == NULL )
+            Ntl_ModelCreatePiWithName( p1, Ntl_ObjFanout0(pObj)->pName );
+    }
+    if ( !fSeq )
+    {
+        Ntl_ModelForEachLatch( p1, pObj, i )
+        {
+            pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
+            if ( pNet == NULL )
+                Ntl_ModelCreatePiWithName( p2, Ntl_ObjFanout0(pObj)->pName );
+        }
+        Ntl_ModelForEachLatch( p2, pObj, i )
+        {
+            pNet = Ntl_ModelFindNet( p1, Ntl_ObjFanout0(pObj)->pName );
+            if ( pNet == NULL )
+                Ntl_ModelCreatePiWithName( p1, Ntl_ObjFanout0(pObj)->pName );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates arrays of combinational inputs in the same order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManDeriveCommonCis( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, int fSeq )
+{
+    Ntl_Mod_t * p1 = Ntl_ManRootModel(pMan1);
+    Ntl_Mod_t * p2 = Ntl_ManRootModel(pMan2);
+    Ntl_Obj_t * pObj;
+    Ntl_Net_t * pNet;
+    int i;
+    if ( fSeq )
+        assert( Ntl_ModelPiNum(p1) == Ntl_ModelPiNum(p2) );
+    else
+        assert( Ntl_ModelCiNum(p1) == Ntl_ModelCiNum(p2) );
+    // order the CIs 
+    Vec_PtrClear( pMan1->vCis );
+    Vec_PtrClear( pMan2->vCis );
+    Ntl_ModelForEachPi( p1, pObj, i )
+    {
+        pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
+        if ( pNet == NULL )
+        {
+            printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" );
+            return;
+        }
+        Vec_PtrPush( pMan1->vCis, pObj );    
+        Vec_PtrPush( pMan2->vCis, pNet->pDriver );    
+    }
+    if ( !fSeq )
+    {
+        Ntl_ModelForEachLatch( p1, pObj, i )
+        {
+            pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
+            if ( pNet == NULL )
+            {
+                printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" );
+                return;
+            }
+            Vec_PtrPush( pMan1->vCis, pObj );    
+            Vec_PtrPush( pMan2->vCis, pNet->pDriver );    
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates arrays of combinational outputs in the same order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManDeriveCommonCos( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, int fSeq )
+{
+    Ntl_Mod_t * p1 = Ntl_ManRootModel(pMan1);
+    Ntl_Mod_t * p2 = Ntl_ManRootModel(pMan2);
+    Ntl_Obj_t * pObj;
+    Ntl_Net_t * pNet;
+    int i;
+//    if ( fSeq )
+//        assert( Ntl_ModelPoNum(p1) == Ntl_ModelPoNum(p2) );
+//    else
+//        assert( Ntl_ModelCoNum(p1) == Ntl_ModelCoNum(p2) );
+    // remember PO in the corresponding net of the second design
+    Ntl_ModelForEachPo( p2, pObj, i )
+        Ntl_ObjFanin0(pObj)->pCopy = pObj;
+    // order the COs 
+    Vec_PtrClear( pMan1->vCos );
+    Vec_PtrClear( pMan2->vCos );
+    Ntl_ModelForEachPo( p1, pObj, i )
+    {
+        pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanin0(pObj)->pName );
+        if ( pNet == NULL )
+        {
+            printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", 
+                Ntl_ObjFanin0(pObj)->pName );
+            continue;
+        }
+        Vec_PtrPush( pMan1->vCos, pObj );    
+        Vec_PtrPush( pMan2->vCos, pNet->pCopy );    
+    }
+    if ( !fSeq )
+    {
+        Ntl_ModelForEachLatch( p2, pObj, i )
+            Ntl_ObjFanin0(pObj)->pCopy = pObj;
+        Ntl_ModelForEachLatch( p1, pObj, i )
+        {
+            pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanin0(pObj)->pName );
+            if ( pNet == NULL )
+            {
+                printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", 
+                    Ntl_ObjFanin0(pObj)->pName );
+                continue;
+            }
+            Vec_PtrPush( pMan1->vCos, pObj );    
+            Vec_PtrPush( pMan2->vCos, pNet->pCopy );    
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares AIGs for combinational equivalence checking.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 )
+{
+    Ntl_Man_t * pMan1, * pMan2;
+    Ntl_Mod_t * pModel1, * pModel2;
+    *ppMan1 = NULL;
+    *ppMan2 = NULL;
+    // read the netlists
+    pMan1 = Ioa_ReadBlif( pFileName1, 1 );
+    pMan2 = Ioa_ReadBlif( pFileName2, 1 );
+    if ( !pMan1 || !pMan2 )
+    {
+        if ( pMan1 )  Ntl_ManFree( pMan1 );
+        if ( pMan2 )  Ntl_ManFree( pMan2 );
+        printf( "Ntl_ManPrepareCec(): Reading designs from file has failed.\n" );
+        return;
+    }
+    // make sure they are compatible
+    pModel1 = Ntl_ManRootModel( pMan1 );
+    pModel2 = Ntl_ManRootModel( pMan2 );
+    if ( Ntl_ModelCiNum(pModel1) != Ntl_ModelCiNum(pModel2) )
+    {
+        printf( "Warning: The number of inputs in the designs is different (%d and %d).\n", 
+            Ntl_ModelCiNum(pModel1), Ntl_ModelCiNum(pModel2) );
+    }
+    if ( Ntl_ModelCoNum(pModel1) != Ntl_ModelCoNum(pModel2) )
+    {
+        printf( "Warning: The number of outputs in the designs is different (%d and %d).\n", 
+            Ntl_ModelCoNum(pModel1), Ntl_ModelCoNum(pModel2) );
+    }
+    // normalize inputs/outputs
+    Ntl_ManCreateMissingInputs( pModel1, pModel2, 0 );
+    Ntl_ManDeriveCommonCis( pMan1, pMan2, 0 );
+    Ntl_ManDeriveCommonCos( pMan1, pMan2, 0 );
+    if ( Vec_PtrSize(pMan1->vCos) == 0 )
+    {
+        printf( "Ntl_ManPrepareCec(): There is no identically-named primary outputs to compare.\n" );
+        if ( pMan1 )  Ntl_ManFree( pMan1 );
+        if ( pMan2 )  Ntl_ManFree( pMan2 );
+        return;
+    }
+    // derive AIGs
+    *ppMan1 = Ntl_ManCollapseForCec( pMan1 );
+    *ppMan2 = Ntl_ManCollapseForCec( pMan2 );
+    // cleanup
+    Ntl_ManFree( pMan1 );
+    Ntl_ManFree( pMan2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares AIGs for sequential equivalence checking.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 )
+{
+    Aig_Man_t * pAig;
+    Ntl_Man_t * pMan1, * pMan2;
+    Ntl_Mod_t * pModel1, * pModel2;
+    // read the netlists
+    pMan1 = Ioa_ReadBlif( pFileName1, 1 );
+    pMan2 = Ioa_ReadBlif( pFileName2, 1 );
+    if ( !pMan1 || !pMan2 )
+    {
+        if ( pMan1 )  Ntl_ManFree( pMan1 );
+        if ( pMan2 )  Ntl_ManFree( pMan2 );
+        printf( "Ntl_ManPrepareSec(): Reading designs from file has failed.\n" );
+        return NULL;
+    }
+    // make sure they are compatible
+    pModel1 = Ntl_ManRootModel( pMan1 );
+    pModel2 = Ntl_ManRootModel( pMan2 );
+    if ( Ntl_ModelLatchNum(pModel1) == 0 || Ntl_ModelLatchNum(pModel2) == 0 )
+    {
+        if ( pMan1 )  Ntl_ManFree( pMan1 );
+        if ( pMan2 )  Ntl_ManFree( pMan2 );
+        printf( "Ntl_ManPrepareSec(): The designs have no latches. Used combinational command \"*cec\".\n" );
+        return NULL;
+    }
+    if ( Ntl_ModelPiNum(pModel1) != Ntl_ModelPiNum(pModel2) )
+    {
+        printf( "Warning: The number of inputs in the designs is different (%d and %d).\n", 
+            Ntl_ModelPiNum(pModel1), Ntl_ModelPiNum(pModel2) );
+    }
+    if ( Ntl_ModelPoNum(pModel1) != Ntl_ModelPoNum(pModel2) )
+    {
+        printf( "Warning: The number of outputs in the designs is different (%d and %d).\n", 
+            Ntl_ModelPoNum(pModel1), Ntl_ModelPoNum(pModel2) );
+    }
+    // normalize inputs/outputs
+    Ntl_ManCreateMissingInputs( pModel1, pModel2, 1 );
+    Ntl_ManDeriveCommonCis( pMan1, pMan2, 1 );
+    Ntl_ManDeriveCommonCos( pMan1, pMan2, 1 );
+    if ( Vec_PtrSize(pMan1->vCos) == 0 )
+    {
+        printf( "Ntl_ManPrepareSec(): There is no identically-named primary outputs to compare.\n" );
+        if ( pMan1 )  Ntl_ManFree( pMan1 );
+        if ( pMan2 )  Ntl_ManFree( pMan2 );
+        return NULL;
+    }
+    // derive AIGs
+    pAig = Ntl_ManCollapseForSec( pMan1, pMan2 );
+    // cleanup
+    pMan1->pAig = pMan2->pAig = NULL;
+    Ntl_ManFree( pMan1 );
+    Ntl_ManFree( pMan2 );
+    return pAig;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 848f113a..9c3666ab 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -467,6 +467,7 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
     int i, nUselessObjects;
+    Ntl_ManCleanup( p );
     assert( Vec_PtrSize(p->vCis) == 0 );
     assert( Vec_PtrSize(p->vCos) == 0 );
     assert( Vec_PtrSize(p->vNodes) == 0 );
@@ -540,7 +541,7 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
         Aig_ObjCreatePo( p->pAig, pNet->pCopy );
     }
     // report the number of dangling objects
-    nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes);
+    nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelLut1Num(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes);
     if ( nUselessObjects )
         printf( "The number of nodes that do not feed into POs = %d.\n", nUselessObjects );
     // cleanup the AIG
@@ -658,7 +659,7 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
+Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq )
 {
     Aig_Man_t * pAig;
     Ntl_Mod_t * pRoot;
@@ -694,6 +695,8 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
         assert( Ntl_ObjFanoutNum(pObj) == 1 );
         pNet = Ntl_ObjFanout0(pObj);
         pNet->pCopy = Aig_ObjCreatePi( p->pAig );
+        if ( fSeq && (pObj->LatchId & 3) == 1 )
+            pNet->pCopy = Aig_Not(pNet->pCopy);
         if ( pNet->nVisits )
         {
             printf( "Ntl_ManCollapse(): Latch output is duplicated or defined as a primary input.\n" );
@@ -721,6 +724,60 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
             printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" );
             return 0;
         }
+        if ( fSeq && (pObj->LatchId & 3) == 1 )
+            Aig_ObjCreatePo( p->pAig, Aig_Not(pNet->pCopy) );
+        else
+            Aig_ObjCreatePo( p->pAig, pNet->pCopy );
+    }
+    // cleanup the AIG
+    Aig_ManCleanup( p->pAig );
+    pAig = p->pAig; p->pAig = NULL;
+    return pAig;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives AIG for CEC.]
+
+  Description [Uses CIs/COs collected in the internal arrays.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p )
+{
+    Aig_Man_t * pAig;
+    Ntl_Obj_t * pObj;
+    Ntl_Net_t * pNet;
+    int i;
+    // create the manager
+    p->pAig = Aig_ManStart( 10000 );
+    p->pAig->pName = Aig_UtilStrsav( p->pName );
+    p->pAig->pSpec = Aig_UtilStrsav( p->pSpec );
+    // set the inputs
+    Ntl_ManForEachCiNet( p, pObj, i )
+    {
+        assert( Ntl_ObjFanoutNum(pObj) == 1 );
+        pNet = Ntl_ObjFanout0(pObj);
+        pNet->pCopy = Aig_ObjCreatePi( p->pAig );
+        if ( pNet->nVisits )
+        {
+            printf( "Ntl_ManCollapseForCec(): Primary input appears twice in the list.\n" );
+            return 0;
+        }
+        pNet->nVisits = 2;
+    }
+    // derive the outputs
+    Ntl_ManForEachCoNet( p, pObj, i )
+    {
+        pNet = Ntl_ObjFanin0(pObj);
+        if ( !Ntl_ManCollapse_rec( p, pNet ) )
+        {
+            printf( "Ntl_ManCollapseForCec(): Error: Combinational loop is detected.\n" );
+            return 0;
+        }
         Aig_ObjCreatePo( p->pAig, pNet->pCopy );
     }
     // cleanup the AIG
@@ -731,6 +788,164 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Performs DFS.]
+
+  Description [Checks for combinational loops. Collects PI/PO nets.
+  Collects nodes in the topological order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
+{
+    Aig_Man_t * pAig;
+    Aig_Obj_t * pMiter;
+    Ntl_Mod_t * pRoot1, * pRoot2;
+    Ntl_Obj_t * pObj;
+    Ntl_Net_t * pNet;
+    Vec_Ptr_t * vPairs;
+    int i;
+    assert( Vec_PtrSize(p1->vCis) > 0 );
+    assert( Vec_PtrSize(p1->vCos) > 0 );
+    assert( Vec_PtrSize(p1->vCis) == Vec_PtrSize(p2->vCis) );
+    assert( Vec_PtrSize(p1->vCos) == Vec_PtrSize(p2->vCos) );
+
+    // create the manager
+    pAig = p1->pAig = p2->pAig = Aig_ManStart( 10000 );
+    pAig->pName = Aig_UtilStrsav( p1->pName );
+    pAig->pSpec = Aig_UtilStrsav( p1->pSpec );
+    vPairs = Vec_PtrStart( 2 * Vec_PtrSize(p1->vCos) );
+    // placehoder output to be used later for the miter output
+    Aig_ObjCreatePo( pAig, Aig_ManConst1(pAig) );
+
+    /////////////////////////////////////////////////////
+    // primary inputs
+    Ntl_ManForEachCiNet( p1, pObj, i )
+    {
+        assert( Ntl_ObjFanoutNum(pObj) == 1 );
+        pNet = Ntl_ObjFanout0(pObj);
+        pNet->pCopy = Aig_ObjCreatePi( pAig );
+        if ( pNet->nVisits )
+        {
+            printf( "Ntl_ManCollapseForSec(): Primary input appears twice in the list.\n" );
+            return 0;
+        }
+        pNet->nVisits = 2;
+    }
+    // latch outputs
+    pRoot1 = Ntl_ManRootModel(p1);
+    Ntl_ModelForEachLatch( pRoot1, pObj, i )
+    {
+        assert( Ntl_ObjFanoutNum(pObj) == 1 );
+        pNet = Ntl_ObjFanout0(pObj);
+        pNet->pCopy = Aig_ObjCreatePi( pAig );
+        if ( (pObj->LatchId & 3) == 1 )
+            pNet->pCopy = Aig_Not(pNet->pCopy);
+        if ( pNet->nVisits )
+        {
+            printf( "Ntl_ManCollapseForSec(): Latch output is duplicated or defined as a primary input.\n" );
+            return 0;
+        }
+        pNet->nVisits = 2;
+    }
+    // derive the outputs
+    Ntl_ManForEachCoNet( p1, pObj, i )
+    {
+        pNet = Ntl_ObjFanin0(pObj);
+        if ( !Ntl_ManCollapse_rec( p1, pNet ) )
+        {
+            printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
+            return 0;
+        }
+//        Aig_ObjCreatePo( pAig, pNet->pCopy );
+        Vec_PtrWriteEntry( vPairs, 2 * i, pNet->pCopy );
+    }
+    // visit the nodes starting from latch inputs outputs
+    Ntl_ModelForEachLatch( pRoot1, pObj, i )
+    {
+        pNet = Ntl_ObjFanin0(pObj);
+        if ( !Ntl_ManCollapse_rec( p1, pNet ) )
+        {
+            printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
+            return 0;
+        }
+        if ( (pObj->LatchId & 3) == 1 )
+            Aig_ObjCreatePo( pAig, Aig_Not(pNet->pCopy) );
+        else
+            Aig_ObjCreatePo( pAig, pNet->pCopy );
+    }
+
+    /////////////////////////////////////////////////////
+    // primary inputs
+    Ntl_ManForEachCiNet( p2, pObj, i )
+    {
+        assert( Ntl_ObjFanoutNum(pObj) == 1 );
+        pNet = Ntl_ObjFanout0(pObj);
+        pNet->pCopy = Aig_ManPi( pAig, i );
+        if ( pNet->nVisits )
+        {
+            printf( "Ntl_ManCollapseForSec(): Primary input appears twice in the list.\n" );
+            return 0;
+        }
+        pNet->nVisits = 2;
+    }
+    // latch outputs
+    pRoot2 = Ntl_ManRootModel(p2);
+    Ntl_ModelForEachLatch( pRoot2, pObj, i )
+    {
+        assert( Ntl_ObjFanoutNum(pObj) == 1 );
+        pNet = Ntl_ObjFanout0(pObj);
+        pNet->pCopy = Aig_ObjCreatePi( pAig );
+        if ( (pObj->LatchId & 3) == 1 )
+            pNet->pCopy = Aig_Not(pNet->pCopy);
+        if ( pNet->nVisits )
+        {
+            printf( "Ntl_ManCollapseForSec(): Latch output is duplicated or defined as a primary input.\n" );
+            return 0;
+        }
+        pNet->nVisits = 2;
+    }
+    // derive the outputs
+    Ntl_ManForEachCoNet( p2, pObj, i )
+    {
+        pNet = Ntl_ObjFanin0(pObj);
+        if ( !Ntl_ManCollapse_rec( p2, pNet ) )
+        {
+            printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
+            return 0;
+        }
+//        Aig_ObjCreatePo( pAig, pNet->pCopy );
+        Vec_PtrWriteEntry( vPairs, 2 * i + 1, pNet->pCopy );
+    }
+    // visit the nodes starting from latch inputs outputs
+    Ntl_ModelForEachLatch( pRoot2, pObj, i )
+    {
+        pNet = Ntl_ObjFanin0(pObj);
+        if ( !Ntl_ManCollapse_rec( p2, pNet ) )
+        {
+            printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
+            return 0;
+        }
+        if ( (pObj->LatchId & 3) == 1 )
+            Aig_ObjCreatePo( pAig, Aig_Not(pNet->pCopy) );
+        else
+            Aig_ObjCreatePo( pAig, pNet->pCopy );
+    }
+
+    /////////////////////////////////////////////////////
+    pMiter = Aig_Miter(pAig, vPairs);
+    Vec_PtrFree( vPairs );
+    Aig_ObjPatchFanin0( pAig, Aig_ManPo(pAig,0), pMiter  );
+    pAig->nRegs = Ntl_ModelLatchNum( pRoot1 ) + Ntl_ModelLatchNum( pRoot2 );
+    Aig_ManCleanup( pAig );
+    return pAig;    
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Increments reference counter of the net.]
 
   Description []
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 7153f081..8a172e6c 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "ntl.h"
+#include "fra.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -30,10 +31,10 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Returns AIG with WB after fraiging.]
+  Synopsis    [Transfers equivalence class info from pAigCol to pAig.]
 
-  Description [pAig points to the nodes of pNew derived using it.
-  pNew points to the nodes of pAigCol derived using it.]
+  Description [pAig points to the nodes of netlist (pNew) derived using it.
+  pNew points to the nodes of the collapsed AIG (pAigCol) derived using it.]
                
   SideEffects []
 
@@ -59,6 +60,9 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
         }
 
     // create mapping from the collapsed manager into the original manager
+    // (each node in the collapsed manager may have more than one equivalent node 
+    // in the original manager; this procedure finds the first node in the original 
+    // manager that is equivalent to the given node in the collapsed manager) 
     pMapBack = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAigCol) );
     memset( pMapBack, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAigCol) );
     Aig_ManForEachObj( pAig, pObj, i )
@@ -115,16 +119,15 @@ Aig_Man_t * Ntl_ManFraig( Ntl_Man_t * p, Aig_Man_t * pAig, int nPartSize, int nC
     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 ) )
+    pNew = Ntl_ManInsertAig( p, pAig );
+    if ( pNew == NULL )
     {
-        Ntl_ManFree( pNew );
         printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
         return NULL;
     }
 
     // collapse the AIG
-    pAigCol = Ntl_ManCollapse( pNew );
+    pAigCol = Ntl_ManCollapse( pNew, 0 );
     // perform fraiging for the given design
     if ( nPartSize == 0 )
         nPartSize = Aig_ManPoNum(pAigCol);
@@ -148,6 +151,153 @@ Aig_Man_t * Ntl_ManFraig( Ntl_Man_t * p, Aig_Man_t * pAig, int nPartSize, int nC
     return pTemp;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs sequential cleanup.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManScl( Ntl_Man_t * p, Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, 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_ManInsertAig( p, pAig );
+    if ( pNew == NULL )
+    {
+        printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
+        return NULL;
+    }
+ 
+    // collapse the AIG
+    pAigCol = Ntl_ManCollapse( pNew, 1 );
+    // perform fraiging for the given design
+    pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+    pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, 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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns AIG with WB after fraiging.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, Aig_Man_t * pAig, int nConfMax, 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_ManInsertAig( p, pAig );
+    if ( pNew == NULL )
+    {
+        printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
+        return NULL;
+    }
+
+    // collapse the AIG
+    pAigCol = Ntl_ManCollapse( pNew, 1 );
+    // perform fraiging for the given design
+    pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+    pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL );
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns AIG with WB after fraiging.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Aig_Man_t * pAig, Fra_Ssw_t * pPars )
+{
+    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_ManInsertAig( p, pAig );
+    if ( pNew == NULL )
+    {
+        printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
+        return NULL;
+    }
+
+    // collapse the AIG
+    pAigCol = Ntl_ManCollapse( pNew, 1 );
+    // perform fraiging for the given design
+    pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+    pTemp = Fra_FraigInduction( pAigCol, pPars );
+    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 10b83660..77fb606a 100644
--- a/src/aig/ntl/ntlInsert.c
+++ b/src/aig/ntl/ntlInsert.c
@@ -40,7 +40,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
+Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
 {
     char Buffer[100];
     Vec_Ptr_t * vCopies;
@@ -50,16 +50,14 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
     Ntl_Net_t * pNet, * pNetCo;
     Ntl_Lut_t * pLut;
     int i, k, nDigits;
+    assert( Vec_PtrSize(p->vCis) == Aig_ManPiNum(pAig) );
+    assert( Vec_PtrSize(p->vCos) == Aig_ManPoNum(pAig) );
+    p = Ntl_ManStartFrom( p );
+    pRoot = Ntl_ManRootModel( p );
+    assert( Ntl_ModelNodeNum(pRoot) == 0 );
     // map the AIG back onto the design
     Ntl_ManForEachCiNet( p, pNet, i )
         pNet->pCopy = Aig_ManPi( pAig, i );
-    Ntl_ManForEachCoNet( p, pNet, i )
-        pNet->pCopy = Aig_ObjChild0( Aig_ManPo( pAig, i ) );
-    // 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;
     // start mapping of AIG nodes into their copies
     vCopies = Vec_PtrStart( Aig_ManObjNumMax(pAig) );
     Ntl_ManForEachCiNet( p, pNet, i )
@@ -101,19 +99,19 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
     Vec_IntFree( vCover );
     // mark CIs and outputs of the registers
     Ntl_ManForEachCiNet( p, pNetCo, i )
-        pNetCo->nVisits = 101; // using "101" is harmless because nVisits can only be 0, 1 or 2
+        pNetCo->fMark = 1;
     // update the CO pointers
     Ntl_ManForEachCoNet( p, pNetCo, i )
     {
-        if ( pNetCo->nVisits == 101 )
+        if ( pNetCo->fMark )
             continue;
-        pNetCo->nVisits = 101;
+        pNetCo->fMark = 1;
         pNet = Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pCopy)->Id );
         pNode = Ntl_ModelCreateNode( pRoot, 1 );
         pNode->pSop = Aig_IsComplement(pNetCo->pCopy)? 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;
+        assert( pNetCo->pDriver == NULL );
         if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
         {
             printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
@@ -121,7 +119,11 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
         }
     }
     Vec_PtrFree( vCopies );
-    return 1;
+    // clean CI/CO marks
+    Ntl_ManUnmarkCiCoNets( p );
+    if ( !Ntl_ManCheck( p ) )
+        printf( "Ntl_ManInsertNtk: The check has failed for design %s.\n", p->pName );
+    return p;
 }
 
 /**Function*************************************************************
@@ -135,7 +137,7 @@ 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 )
+Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
 {
     char Buffer[100];
     Ntl_Mod_t * pRoot;
@@ -145,17 +147,13 @@ int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
     int i, nDigits, Counter;
     assert( Vec_PtrSize(p->vCis) == Aig_ManPiNum(pAig) );
     assert( Vec_PtrSize(p->vCos) == Aig_ManPoNum(pAig) );
+    p = Ntl_ManStartFrom( p );
+    pRoot = Ntl_ManRootModel( p );
+    assert( Ntl_ModelNodeNum(pRoot) == 0 );
     // 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 )
     {
@@ -213,13 +211,13 @@ int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
     }
     // mark CIs and outputs of the registers
     Ntl_ManForEachCiNet( p, pNetCo, i )
-        pNetCo->nVisits = 101;
+        pNetCo->fMark = 1;
     // update the CO pointers
     Ntl_ManForEachCoNet( p, pNetCo, i )
     {
-        if ( pNetCo->nVisits == 101 )
+        if ( pNetCo->fMark )
             continue;
-        pNetCo->nVisits = 101;
+        pNetCo->fMark = 1;
         // get the corresponding PO and its driver
         pObj = Aig_ManPo( pAig, i );
         pFanin = Aig_ObjFanin0( pObj );
@@ -229,14 +227,18 @@ int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
         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;
+        assert( pNetCo->pDriver == NULL );
         if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
         {
-            printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
+            printf( "Ntl_ManInsertAig(): Internal error: PO net has more than one fanin.\n" );
             return 0;
         }
     }
-    return 1;
+    // clean CI/CO marks
+    Ntl_ManUnmarkCiCoNets( p );
+    if ( !Ntl_ManCheck( p ) )
+        printf( "Ntl_ManInsertAig: The check has failed for design %s.\n", p->pName );
+    return p;
 }
 
 
@@ -251,7 +253,7 @@ int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
+Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
 {
     char Buffer[100];
     Vec_Ptr_t * vObjs;
@@ -265,16 +267,12 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
     unsigned * pTruth;
     assert( Vec_PtrSize(p->vCis) == Nwk_ManCiNum(pNtk) );
     assert( Vec_PtrSize(p->vCos) == Nwk_ManCoNum(pNtk) );
+    p = Ntl_ManStartFrom( p );
+    pRoot = Ntl_ManRootModel( p );
+    assert( Ntl_ModelNodeNum(pRoot) == 0 );
     // set the correspondence between the PI/PO nodes
     Ntl_ManForEachCiNet( p, pNet, i )
         Nwk_ManCi( pNtk, i )->pCopy = 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 a new node for each LUT
     vTruth = Vec_IntAlloc( 1 << 16 );
     vCover = Vec_IntAlloc( 1 << 16 );
@@ -298,7 +296,7 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
                 pNet = pFanin->pCopy;
                 if ( pNet == NULL )
                 {
-                    printf( "Ntl_ManInsert(): Internal error: Net not found.\n" );
+                    printf( "Ntl_ManInsertNtk(): Internal error: Net not found.\n" );
                     return 0;
                 }
                 Ntl_ObjSetFanin( pNode, pNet, k );
@@ -307,13 +305,13 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
         sprintf( Buffer, "lut%0*d", nDigits, i );
         if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
         {
-            printf( "Ntl_ManInsert(): Internal error: Intermediate net name is not unique.\n" );
+            printf( "Ntl_ManInsertNtk(): Internal error: Intermediate net name is not unique.\n" );
             return 0;
         }
         pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer );
         if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
         {
-            printf( "Ntl_ManInsert(): Internal error: Net has more than one fanin.\n" );
+            printf( "Ntl_ManInsertNtk(): Internal error: Net has more than one fanin.\n" );
             return 0;
         }
         pObj->pCopy = pNet;
@@ -323,13 +321,13 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
     Vec_IntFree( vTruth );
     // mark CIs and outputs of the registers
     Ntl_ManForEachCiNet( p, pNetCo, i )
-        pNetCo->nVisits = 101;
+        pNetCo->fMark = 1;
     // update the CO pointers
     Ntl_ManForEachCoNet( p, pNetCo, i )
     {
-        if ( pNetCo->nVisits == 101 )
+        if ( pNetCo->fMark )
             continue;
-        pNetCo->nVisits = 101;
+        pNetCo->fMark = 1;
         // get the corresponding PO and its driver
         pObj = Nwk_ManCo( pNtk, i );
         pFanin = Nwk_ObjFanin0( pObj );
@@ -339,14 +337,18 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
         pNode->pSop = pObj->fCompl /*Aig_IsComplement(pNetCo->pCopy)*/? 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;
+        assert( pNetCo->pDriver == NULL );
         if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
         {
-            printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
+            printf( "Ntl_ManInsertNtk(): Internal error: PO net has more than one fanin.\n" );
             return 0;
         }
     }
-    return 1;
+    // clean CI/CO marks
+    Ntl_ManUnmarkCiCoNets( p );
+    if ( !Ntl_ManCheck( p ) )
+        printf( "Ntl_ManInsertNtk: The check has failed for design %s.\n", p->pName );
+    return p;
 }
 
 
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index 83219df7..82131091 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -61,7 +61,36 @@ Ntl_Man_t * Ntl_ManAlloc( char * pFileName )
 
 /**Function*************************************************************
 
-  Synopsis    [Duplicates the interface of the top level model.]
+  Synopsis    [Cleanups extended representation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManCleanup( Ntl_Man_t * p )
+{
+    Vec_PtrClear( p->vCis );
+    Vec_PtrClear( p->vCos );
+    Vec_PtrClear( p->vNodes );
+    Vec_IntClear( p->vBox1Cos );
+    if ( p->pAig )
+    {
+        Aig_ManStop( p->pAig );
+        p->pAig = NULL;
+    }
+    if ( p->pManTime )
+    {
+        Tim_ManStop( p->pManTime );
+        p->pManTime = NULL;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the design without the nodes of the root model.]
 
   Description []
                
@@ -72,12 +101,36 @@ Ntl_Man_t * Ntl_ManAlloc( char * pFileName )
 ***********************************************************************/
 Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * pOld )
 {
-    return NULL;
+    Ntl_Man_t * pNew;
+    Ntl_Mod_t * pModel;
+    Ntl_Obj_t * pBox;
+    Ntl_Net_t * pNet;
+    int i, k;
+    pNew = Ntl_ManAlloc( pOld->pSpec );
+    Vec_PtrForEachEntry( pOld->vModels, pModel, i )
+        if ( i == 0 )
+        {
+            Ntl_ManMarkCiCoNets( pOld );
+            pModel->pCopy = Ntl_ModelStartFrom( pNew, pModel );
+            Ntl_ManUnmarkCiCoNets( pOld );
+        }
+        else
+            pModel->pCopy = Ntl_ModelDup( pNew, pModel );
+    Vec_PtrForEachEntry( pOld->vModels, pModel, i )
+        Ntl_ModelForEachBox( pModel, pBox, k )
+            ((Ntl_Obj_t *)pBox->pCopy)->pImplem = pBox->pImplem->pCopy;
+    Ntl_ManForEachCiNet( pOld, pNet, i )
+        Vec_PtrPush( pNew->vCis, pNet->pCopy );
+    Ntl_ManForEachCoNet( pOld, pNet, i )
+        Vec_PtrPush( pNew->vCos, pNet->pCopy );
+    if ( pOld->pManTime )
+        pNew->pManTime = Tim_ManDup( pOld->pManTime, 0 );
+    return pNew;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Duplicates the interface of the top level model.]
+  Synopsis    [Duplicates the design.]
 
   Description []
                
@@ -144,6 +197,22 @@ void Ntl_ManFree( Ntl_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if the design is combinational.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManIsComb( Ntl_Man_t * p )          
+{ 
+    return Ntl_ModelLatchNum(Ntl_ManRootModel(p)) == 0; 
+} 
+
+/**Function*************************************************************
+
   Synopsis    [Find the model with the given name.]
 
   Description []
@@ -178,15 +247,18 @@ void Ntl_ManPrintStats( Ntl_Man_t * p )
 {
     Ntl_Mod_t * pRoot;
     pRoot = Ntl_ManRootModel( p );
-    printf( "%-15s : ",       p->pName );
-    printf( "pi = %5d  ",    Ntl_ModelPiNum(pRoot) );
-    printf( "po = %5d  ",    Ntl_ModelPoNum(pRoot) );
-    printf( "lat = %5d  ", Ntl_ModelLatchNum(pRoot) );
-    printf( "node = %5d  ",  Ntl_ModelNodeNum(pRoot) );
-    printf( "box = %4d  ",   Ntl_ModelBoxNum(pRoot) );
-    printf( "mod = %3d",   Vec_PtrSize(p->vModels) );
+    printf( "%-15s : ",        p->pName );
+    printf( "pi = %5d  ",      Ntl_ModelPiNum(pRoot) );
+    printf( "po = %5d  ",      Ntl_ModelPoNum(pRoot) );
+    printf( "lat = %5d  ",     Ntl_ModelLatchNum(pRoot) );
+    printf( "node = %5d  ",    Ntl_ModelNodeNum(pRoot) );
+    printf( "inv/buf = %5d  ", Ntl_ModelLut1Num(pRoot) );
+    printf( "box = %4d  ",     Ntl_ModelBoxNum(pRoot) );
+    printf( "mod = %3d  ",     Vec_PtrSize(p->vModels) );
+    printf( "net = %d",       Ntl_ModelCountNets(pRoot) );
     printf( "\n" );
     fflush( stdout );
+    assert( Ntl_ModelLut1Num(pRoot) == Ntl_ModelCountLut1(pRoot) );
 }
 
 /**Function*************************************************************
@@ -237,6 +309,50 @@ Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the model without nodes but with CI/CO nets.]
+
+  Description [The CI/CO nets of the old model should be marked before 
+  calling this procedure.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
+{
+    Ntl_Mod_t * pModelNew;
+    Ntl_Net_t * pNet;
+    Ntl_Obj_t * pObj;
+    int i, k;
+    pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName );
+    Ntl_ModelForEachNet( pModelOld, pNet, i )
+        if ( pNet->fMark )
+            pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName );
+        else
+            pNet->pCopy = NULL;
+    Ntl_ModelForEachObj( pModelOld, pObj, i )
+    {
+        if ( Ntl_ObjIsNode(pObj) )
+            continue;
+        pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj );
+        Ntl_ObjForEachFanin( pObj, pNet, k )
+            if ( pNet->pCopy != NULL )
+                Ntl_ObjSetFanin( pObj->pCopy, pNet->pCopy, k );
+        Ntl_ObjForEachFanout( pObj, pNet, k )
+            if ( pNet->pCopy != NULL )
+                Ntl_ObjSetFanout( pObj->pCopy, pNet->pCopy, k );
+        if ( Ntl_ObjIsLatch(pObj) )
+            ((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId;
+    }
+    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;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates the model.]
 
   Description []
@@ -286,6 +402,7 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
 ***********************************************************************/
 void Ntl_ModelFree( Ntl_Mod_t * p )
 {
+    assert( Ntl_ManCheckNetsAreNotMarked(p) );
     if ( p->vRequireds )  Vec_IntFree( p->vRequireds );
     if ( p->vArrivals )   Vec_IntFree( p->vArrivals );
     if ( p->vDelays )     Vec_IntFree( p->vDelays );
diff --git a/src/aig/ntl/ntlObj.c b/src/aig/ntl/ntlObj.c
index ad43623a..68b5cfe8 100644
--- a/src/aig/ntl/ntlObj.c
+++ b/src/aig/ntl/ntlObj.c
@@ -131,7 +131,10 @@ Ntl_Obj_t * Ntl_ModelCreateNode( Ntl_Mod_t * pModel, int nFanins )
     p->Type     = NTL_OBJ_NODE;
     p->nFanins  = nFanins;
     p->nFanouts = 1;
-    pModel->nObjs[NTL_OBJ_NODE]++;
+    if ( nFanins == 1 )
+        pModel->nObjs[NTL_OBJ_LUT1]++;
+    else
+        pModel->nObjs[NTL_OBJ_NODE]++;
     return p;
 }
 
@@ -188,6 +191,30 @@ Ntl_Obj_t * Ntl_ModelDupObj( Ntl_Mod_t * pModel, Ntl_Obj_t * pOld )
     return pNew;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the primary input with the given name.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Obj_t * Ntl_ModelCreatePiWithName( Ntl_Mod_t * pModel, char * pName )
+{
+    Ntl_Obj_t * pObj;
+    Ntl_Net_t * pNet;
+    pNet = Ntl_ModelFindOrCreateNet( pModel, pName );
+    if ( pNet->pDriver )
+        return NULL;
+    pObj = Ntl_ModelCreatePi( pModel );
+    Ntl_ModelSetNetDriver( pObj, pNet );
+    return pObj;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Allocates memory and copies the name into it.]
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index ce3a2051..dd74f9ba 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -109,7 +109,7 @@ Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck )
     FILE * pFile;
     Ioa_ReadMan_t * p;
     Ntl_Man_t * pDesign;
-    int nNodes;
+//    int nNodes;
 
     // check that the file is available
     pFile = fopen( pFileName, "rb" );
@@ -166,8 +166,8 @@ 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 );
+//    if ( (nNodes = Ntl_ManReconnectCoDrivers(pDesign)) )
+//        printf( "The design was transformed by removing %d buf/inv CO drivers.\n", nNodes );
 //Ioa_WriteBlif( pDesign, "_temp_.blif" );
     return pDesign;
 }
diff --git a/src/aig/ntl/ntlSweep.c b/src/aig/ntl/ntlSweep.c
new file mode 100644
index 00000000..3b9cd61f
--- /dev/null
+++ b/src/aig/ntl/ntlSweep.c
@@ -0,0 +1,165 @@
+/**CFile****************************************************************
+
+  FileName    [ntlSweep.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Performs structural sweep of the netlist.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntlSweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Detects logic that does not fanout into POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManSweepMark_rec( Ntl_Man_t * p, Ntl_Obj_t * pObj )
+{
+    Ntl_Net_t * pNet;
+    int i;
+    if ( pObj->fMark )
+        return;
+    pObj->fMark = 1;
+    Ntl_ObjForEachFanin( pObj, pNet, i )
+        Ntl_ManSweepMark_rec( p, pNet->pDriver );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Detects logic that does not fanout into POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManSweepMark( Ntl_Man_t * p )
+{
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pObj;
+    int i;
+    // get the root model
+    pRoot = Ntl_ManRootModel( p );
+    // clear net visited flags
+    Ntl_ModelForEachObj( pRoot, pObj, i )
+        assert( pObj->fMark == 0 );
+    // label the primary inputs
+    Ntl_ModelForEachPi( pRoot, pObj, i )
+        pObj->fMark = 1;
+    // start from the primary outputs
+    Ntl_ModelForEachPo( pRoot, pObj, i )
+        Ntl_ManSweepMark_rec( p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives new netlist by sweeping current netlist with the current AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Man_t * Ntl_ManSweep( Ntl_Man_t * p, Aig_Man_t * pAig, int fVerbose )
+{
+    int nObjsOld[NTL_OBJ_VOID];
+    Ntl_Man_t * pNew;
+    Ntl_Mod_t * pRoot;
+    Ntl_Net_t * pNet;
+    Ntl_Obj_t * pObj;
+    int i, k, nNetsOld;
+
+    // insert the AIG into the netlist
+    pNew = Ntl_ManInsertAig( p, pAig );
+    if ( pNew == NULL )
+    {
+        printf( "Ntl_ManSweep(): Inserting AIG has failed.\n" );
+        return NULL;
+    }
+
+    // remember the number of objects
+    pRoot = Ntl_ManRootModel( pNew );
+    for ( i = 0; i < NTL_OBJ_VOID; i++ )
+        nObjsOld[i] = pRoot->nObjs[i];
+    nNetsOld = Ntl_ModelCountNets(pRoot);
+
+    // mark the nets that do not fanout into POs
+    Ntl_ManSweepMark( pNew );
+
+    // remove the useless objects and their nets
+    Ntl_ModelForEachObj( pRoot, pObj, i )
+    {
+        if ( pObj->fMark )
+        {
+            pObj->fMark = 0;
+            continue;
+        }
+        // remove the fanout nets
+        Ntl_ObjForEachFanout( pObj, pNet, k )
+            Ntl_ModelDeleteNet( pRoot, Ntl_ObjFanout0(pObj) );
+        // remove the object
+        if ( Ntl_ObjIsNode(pObj) && Ntl_ObjFaninNum(pObj) == 1 )
+            pRoot->nObjs[NTL_OBJ_LUT1]--;
+        else
+            pRoot->nObjs[pObj->Type]--;
+        Vec_PtrWriteEntry( pRoot->vObjs, pObj->Id, NULL );
+        pObj->Id = NTL_OBJ_NONE;
+    }
+
+    // print detailed statistics of sweeping
+    if ( fVerbose )
+    {
+        printf( "Sweep:" );
+        printf( "  Node = %d (%4.1f %%)", 
+            nObjsOld[NTL_OBJ_NODE] - pRoot->nObjs[NTL_OBJ_NODE],
+            !nObjsOld[NTL_OBJ_NODE]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_NODE] - pRoot->nObjs[NTL_OBJ_NODE]) / nObjsOld[NTL_OBJ_NODE] );
+        printf( "  Buf/Inv = %d (%4.1f %%)", 
+            nObjsOld[NTL_OBJ_LUT1] - pRoot->nObjs[NTL_OBJ_LUT1],
+            !nObjsOld[NTL_OBJ_LUT1]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_LUT1] - pRoot->nObjs[NTL_OBJ_LUT1]) / nObjsOld[NTL_OBJ_LUT1] );
+        printf( "  Lat = %d (%4.1f %%)", 
+            nObjsOld[NTL_OBJ_LATCH] - pRoot->nObjs[NTL_OBJ_LATCH],
+            !nObjsOld[NTL_OBJ_LATCH]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_LATCH] - pRoot->nObjs[NTL_OBJ_LATCH]) / nObjsOld[NTL_OBJ_LATCH] );
+        printf( "  Box = %d (%4.1f %%)", 
+            nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX],
+            !nObjsOld[NTL_OBJ_BOX]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX]) / nObjsOld[NTL_OBJ_BOX] );
+        printf( "\n" );
+//        printf( "Also, sweep reduced %d nets.\n", nNetsOld - Ntl_ModelCountNets(pRoot) );
+    }
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c
index df982481..07794492 100644
--- a/src/aig/ntl/ntlTable.c
+++ b/src/aig/ntl/ntlTable.c
@@ -239,6 +239,26 @@ int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Finds or creates the net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCountNets( Ntl_Mod_t * p )
+{
+    Ntl_Net_t * pNet;
+    int i, Counter = 0;
+    Ntl_ModelForEachNet( p, pNet, i )
+        Counter++;
+    return Counter;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c
index b13dd3a7..626bcbe1 100644
--- a/src/aig/ntl/ntlUtil.c
+++ b/src/aig/ntl/ntlUtil.c
@@ -30,7 +30,28 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if netlist was written by ABC with added bufs/invs.]
+  Synopsis    [Counts COs that are connected to the internal nodes through invs/bufs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot )
+{
+    Ntl_Obj_t * pObj;
+    int i, Counter = 0;
+    Ntl_ModelForEachNode( pRoot, pObj, i )
+        if ( Ntl_ObjFaninNum(pObj) == 1 )
+            Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Connects COs to the internal nodes other than inv/bufs.]
 
   Description [Should be called immediately after reading from file.]
                
@@ -39,6 +60,63 @@
   SeeAlso     []
 
 ***********************************************************************/
+int Ntl_ManCountSimpleCoDriversOne( Ntl_Net_t * pNetCo )
+{
+    Ntl_Net_t * pNetFanin;
+    // skip the case when the net is not driven by a node
+    if ( !Ntl_ObjIsNode(pNetCo->pDriver) )
+        return 0;
+    // skip the case when the node is not an inv/buf
+    if ( Ntl_ObjFaninNum(pNetCo->pDriver) != 1 )
+        return 0;
+    // skip the case when the second-generation driver is not a node
+    pNetFanin = Ntl_ObjFanin0(pNetCo->pDriver);
+    if ( !Ntl_ObjIsNode(pNetFanin->pDriver) )
+        return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts COs that are connected to the internal nodes through invs/bufs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p )
+{
+    Ntl_Net_t * pNetCo;
+    Ntl_Obj_t * pObj;
+    Ntl_Mod_t * pRoot;
+    int i, k, Counter;
+    Counter = 0;
+    pRoot = Ntl_ManRootModel( p );
+    Ntl_ModelForEachPo( pRoot, pObj, i )
+        Counter += Ntl_ManCountSimpleCoDriversOne( Ntl_ObjFanin0(pObj) );
+    Ntl_ModelForEachLatch( pRoot, pObj, i )
+        Counter += Ntl_ManCountSimpleCoDriversOne( Ntl_ObjFanin0(pObj) );
+    Ntl_ModelForEachBox( pRoot, pObj, i )
+        Ntl_ObjForEachFanin( pObj, pNetCo, k )
+            Counter += Ntl_ManCountSimpleCoDriversOne( pNetCo );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes the CO drivers that are bufs/invs.]
+
+  Description [Should be called immediately after reading from file.]
+               
+  SideEffects [This procedure does not work because the internal net
+  (pNetFanin) may have other drivers.]
+
+  SeeAlso     []
+
+***********************************************************************/
 int Ntl_ManTransformCoDrivers( Ntl_Man_t * p )
 {
     Vec_Ptr_t * vCoNets;
@@ -110,7 +188,71 @@ int Ntl_ManTransformCoDrivers( Ntl_Man_t * p )
         Counter++;
     }
     Vec_PtrFree( vCoNets );
-    pRoot->nObjs[NTL_OBJ_NODE] -= Counter;
+    pRoot->nObjs[NTL_OBJ_LUT1] -= Counter;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Connects COs to the internal nodes other than inv/bufs.]
+
+  Description [Should be called immediately after reading from file.]
+               
+  SideEffects [This procedure does not work because the internal net
+  (pNetFanin) may have other drivers.]
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManReconnectCoDriverOne( Ntl_Net_t * pNetCo )
+{
+    Ntl_Net_t * pNetFanin;
+    // skip the case when the net is not driven by a node
+    if ( !Ntl_ObjIsNode(pNetCo->pDriver) )
+        return 0;
+    // skip the case when the node is not an inv/buf
+    if ( Ntl_ObjFaninNum(pNetCo->pDriver) != 1 )
+        return 0;
+    // skip the case when the second-generation driver is not a node
+    pNetFanin = Ntl_ObjFanin0(pNetCo->pDriver);
+    if ( !Ntl_ObjIsNode(pNetFanin->pDriver) )
+        return 0;
+    // set the complemented attribute of the net
+    pNetCo->fCompl = (int)(pNetCo->pDriver->pSop[0] == '0');
+    // drive the CO net with the second-generation driver
+    pNetCo->pDriver = NULL;
+    pNetFanin->pDriver->pFanio[pNetFanin->pDriver->nFanins] = NULL;
+    if ( !Ntl_ModelSetNetDriver( pNetFanin->pDriver, pNetCo ) )
+        printf( "Ntl_ManReconnectCoDriverOne(): Cannot connect the net.\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Connects COs to the internal nodes other than inv/bufs.]
+
+  Description [Should be called immediately after reading from file.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManReconnectCoDrivers( Ntl_Man_t * p )
+{
+    Ntl_Net_t * pNetCo;
+    Ntl_Obj_t * pObj;
+    Ntl_Mod_t * pRoot;
+    int i, k, Counter;
+    Counter = 0;
+    pRoot = Ntl_ManRootModel( p );
+    Ntl_ModelForEachPo( pRoot, pObj, i )
+        Counter += Ntl_ManReconnectCoDriverOne( Ntl_ObjFanin0(pObj) );
+    Ntl_ModelForEachLatch( pRoot, pObj, i )
+        Counter += Ntl_ManReconnectCoDriverOne( Ntl_ObjFanin0(pObj) );
+    Ntl_ModelForEachBox( pRoot, pObj, i )
+        Ntl_ObjForEachFanin( pObj, pNetCo, k )
+            Counter += Ntl_ManReconnectCoDriverOne( pNetCo );
     return Counter;
 }
 
@@ -158,6 +300,68 @@ Vec_Ptr_t * Ntl_ManCollectCoNames( Ntl_Man_t * p )
     return vNames;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Marks the CI/CO nets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManMarkCiCoNets( Ntl_Man_t * p )
+{
+    Ntl_Net_t * pNet;
+    int i;
+    Ntl_ManForEachCiNet( p, pNet, i )
+        pNet->fMark = 1;
+    Ntl_ManForEachCoNet( p, pNet, i )
+        pNet->fMark = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unmarks the CI/CO nets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p )
+{
+    Ntl_Net_t * pNet;
+    int i;
+    Ntl_ManForEachCiNet( p, pNet, i )
+        pNet->fMark = 0;
+    Ntl_ManForEachCoNet( p, pNet, i )
+        pNet->fMark = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unmarks the CI/CO nets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel )
+{
+    Ntl_Net_t * pNet;
+    int i;
+    Ntl_ModelForEachNet( pModel, pNet, i )
+        assert( pNet->fMark == 0 );
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/nwk/nwkMan.c b/src/aig/nwk/nwkMan.c
index 9c2c5ed8..a1f20a8e 100644
--- a/src/aig/nwk/nwkMan.c
+++ b/src/aig/nwk/nwkMan.c
@@ -100,7 +100,6 @@ void Nwk_ManPrintLutSizes( Nwk_Man_t * p, If_Lib_t * pLutLib )
     printf( "LUTs by size: " );
     for ( i = 0; i <= pLutLib->LutMax; i++ )
         printf( "%d:%d ", i, Counters[i] );
-    printf( "\n" );
 }
 
 /**Function*************************************************************
@@ -124,6 +123,7 @@ void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib )
     printf( "co = %5d  ",    Nwk_ManCoNum(p) );
     printf( "lat = %5d  ",   Nwk_ManLatchNum(p) );
     printf( "node = %5d  ",  Nwk_ManNodeNum(p) );
+    printf( "edge = %5d  ",  Nwk_ManGetTotalFanins(p) );
     printf( "aig = %6d  ",   Nwk_ManGetAigNodeNum(p) );
     printf( "lev = %3d  ",   Nwk_ManLevel(p) );
 //    printf( "lev2 = %3d  ",  Nwk_ManLevelBackup(p) );
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index 025d2001..a78632d2 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -725,7 +725,8 @@ bool Abc_NtkCompareBoxes( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
 
   Description []
                
-  SideEffects []
+  SideEffects [Ordering POs by name is a very bad idea! It destroys
+  the natural order of the logic in the circuit.]
 
   SeeAlso     []
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index add5a7e0..e8ad6610 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -218,6 +218,7 @@ static int Abc_CommandAbc8Lutpack    ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandAbc8Balance    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Speedup    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Fraig      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Sweep      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Cec        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Scl        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Lcorr      ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -456,6 +457,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC8",         "*b",            Abc_CommandAbc8Balance,      0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*speedup",      Abc_CommandAbc8Speedup,      0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*fraig",        Abc_CommandAbc8Fraig,        0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*sw",           Abc_CommandAbc8Sweep,        0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*cec",          Abc_CommandAbc8Cec,          0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*scl",          Abc_CommandAbc8Scl,          0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*lcorr",        Abc_CommandAbc8Lcorr,        0 );
@@ -14868,8 +14870,8 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     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_ManInsertNtk( void * p, void * pNtk );
+    extern void * Ntl_ManInsertAig( void * p, Aig_Man_t * pAig );
     extern void * Ntl_ManDup( void * pOld );
     extern void Ntl_ManFree( void * p );
 
@@ -14895,16 +14897,19 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     // create the design to write
-    pTemp = Ntl_ManDup( pAbc->pAbc8Ntl );
+    pFileName = argv[globalUtilOptind];
     if ( fAig )
     {
         if ( pAbc->pAbc8Aig != NULL )
         {
-            if ( !Ntl_ManInsertAig( pTemp, pAbc->pAbc8Aig ) )
+            pTemp = Ntl_ManInsertAig( pAbc->pAbc8Ntl, pAbc->pAbc8Aig );
+            if ( pTemp == NULL )
             {
                 printf( "Abc_CommandAbc8Write(): Inserting AIG has failed.\n" );
                 return 1;
             }
+            Ioa_WriteBlif( pTemp, pFileName );
+            Ntl_ManFree( pTemp );
         }
         else
         {
@@ -14916,19 +14921,22 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         if ( pAbc->pAbc8Nwk != NULL ) 
         {
-            if ( !Ntl_ManInsertNtk( pTemp, pAbc->pAbc8Nwk ) )
+            pTemp = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
+            if ( pTemp == NULL )
             {
                 printf( "Abc_CommandAbc8Write():  Inserting mapped network has failed.\n" );
                 return 1;
             }
+            Ioa_WriteBlif( pTemp, pFileName );
+            Ntl_ManFree( pTemp );
         }
         else
+        {
+            pTemp = pAbc->pAbc8Ntl;
             printf( "Writing the original design.\n" );
+            Ioa_WriteBlif( pTemp, pFileName );
+        }
     }
-    // get the input file name
-    pFileName = argv[globalUtilOptind];
-    Ioa_WriteBlif( pTemp, pFileName );
-    Ntl_ManFree( pTemp );
     return 0;
 
 usage:
@@ -15093,8 +15101,6 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
     If_Par_t Pars, * pPars = &Pars;
     void * pNtkNew;
     int c;
-    extern int Ntl_ManInsertTest( void * p, Aig_Man_t * pAig );
-    extern int Ntl_ManInsertTestIf( void * p, Aig_Man_t * pAig );
     extern void * Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars );
     extern Tim_Man_t * Ntl_ManReadTimeMan( void * p );
     extern If_Lib_t * If_SetSimpleLutLib( int nLutSize );
@@ -15126,15 +15132,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc8Write(): There is no AIG to map.\n" );
         return 1;
     }
-/*
-    // get the input file name
-    if ( !Ntl_ManInsertTestIf( pAbc->pAbc8Ntl, pAbc->pAbc8Aig ) )
-//    if ( !Ntl_ManInsertTest( pAbc->pAbc8Ntl, pAbc->pAbc8Aig ) )
-    {
-        printf( "Abc_CommandAbc8Write(): Tranformation of the netlist has failed.\n" );
-        return 1;
-    }
-*/
+
     pNtkNew = Nwk_MappingIf( pAbc->pAbc8Aig, Ntl_ManReadTimeMan(pAbc->pAbc8Ntl), pPars );
     if ( pNtkNew == NULL )
     {
@@ -16053,6 +16051,78 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    void * pNtlNew;
+    int fVerbose;
+    int c;
+    extern void * Ntl_ManSweep( void * p, Aig_Man_t * pAig, int fVerbose );
+    extern Aig_Man_t * Ntl_ManExtract( void * p );
+
+    // set defaults
+    fVerbose = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Sweep(): There is no design to sweep.\n" );
+        return 1;
+    }
+    if ( pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8Sweep(): There is no AIG to use.\n" );
+        return 1;
+    }
+
+    // sweep the current design
+    pNtlNew = Ntl_ManSweep( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, fVerbose );
+    if ( pNtlNew == NULL )
+    {
+        printf( "Abc_CommandAbc8Sweep(): Sweeping has failed.\n" );
+        return 1;
+    }
+    // replace
+    Abc_FrameClearDesign(); 
+    pAbc->pAbc8Ntl = pNtlNew;
+    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
+    if ( pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8Sweep(): AIG extraction has failed.\n" );
+        return 1;
+    }
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: *sw [-h]\n" );
+    fprintf( stdout, "\t        reads the design with whiteboxes\n" );
+    fprintf( stdout, "\t-v    : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Aig_Man_t * pAig1, * pAig2;
@@ -16064,11 +16134,12 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nConfLimit;
     int fSmart;
     int nPartSize;
-    extern Aig_Man_t * Ntl_ManCollapse( void * p );
+    extern Aig_Man_t * Ntl_ManCollapse( void * p, int fSeq );
     extern void * Ntl_ManDup( void * pOld );
     extern void Ntl_ManFree( void * p );
-    extern int Ntl_ManInsertNtk( void * p, void * pNtk );
+    extern void * Ntl_ManInsertNtk( void * p, void * pNtk );
 
+    extern void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 );
     extern int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
 
     // set defaults
@@ -16116,31 +16187,42 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     pArgvNew = argv + globalUtilOptind;
     nArgcNew = argc - globalUtilOptind;
-    if ( nArgcNew != 0 )
+    if ( nArgcNew != 0 && nArgcNew != 2 )
     {
-        printf( "Currently can only compare current network against the spec.\n" );
+        printf( "Currently can only compare current mapped network against the spec, or designs derived from two files.\n" );
         return 0;
     }
+    if ( nArgcNew == 2 )
+    {
+        Ntl_ManPrepareCec( pArgvNew[0], pArgvNew[1], &pAig1, &pAig2 );
+        if ( !pAig1 || !pAig2 )
+            return 1;
+        Fra_FraigCecTop( pAig1, pAig2, nConfLimit, nPartSize, fSmart, fVerbose );
+        Aig_ManStop( pAig1 );
+        Aig_ManStop( pAig2 );
+        return 0;
+    }
+
     if ( pAbc->pAbc8Ntl == NULL )
     {
         printf( "Abc_CommandAbc8Cec(): There is no design to verify.\n" );
-        return 0;
+        return 1;
     }
     if ( pAbc->pAbc8Nwk == NULL )
     {
         printf( "Abc_CommandAbc8Cec(): There is no mapped network to verify.\n" );
-        return 0;
+        return 1;
     }
 
     // derive AIGs
-    pAig1 = Ntl_ManCollapse( pAbc->pAbc8Ntl );
-    pTemp = Ntl_ManDup( pAbc->pAbc8Ntl );
-    if ( !Ntl_ManInsertNtk( pTemp, pAbc->pAbc8Nwk ) )
+    pAig1 = Ntl_ManCollapse( pAbc->pAbc8Ntl, 0 );
+    pTemp = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
+    if ( pTemp == NULL )
     {
         printf( "Abc_CommandAbc8Cec(): Inserting the design has failed.\n" );
         return 1;
     }
-    pAig2 = Ntl_ManCollapse( pTemp );
+    pAig2 = Ntl_ManCollapse( pTemp, 0 );
     Ntl_ManFree( pTemp );
 
     // perform verification
@@ -16160,7 +16242,7 @@ usage:
     fprintf( stdout, "\tfile1  : (optional) the file with the first network\n");
     fprintf( stdout, "\tfile2  : (optional) the file with the second network\n");
     fprintf( stdout, "\t         if no files are given, uses the current network and its spec\n");
-    fprintf( stdout, "\t         if one file is given, uses the current network and the file\n");
+    fprintf( stdout, "\t         if two files are given, compares designs derived from files\n");
     return 1;
 }
 
@@ -16177,7 +16259,77 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    Aig_Man_t * pAigNew;
+    int c;
+    int fLatchConst;
+    int fLatchEqual;
+    int fVerbose;
+    extern Aig_Man_t * Ntl_ManScl( void * p, Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose );
+    extern int Ntl_ManIsComb( void * p );
+
+    // set defaults
+    fLatchConst = 1;
+    fLatchEqual = 1;
+    fVerbose    = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cevh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'c':
+            fLatchConst ^= 1;
+            break;
+        case 'e':
+            fLatchEqual ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Scl(): There is no design to SAT sweep.\n" );
+        return 1;
+    }
+    if ( pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8Scl(): There is no AIG to SAT sweep.\n" );
+        return 1;
+    }
+
+    if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
+    {
+        fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
+        return 0;
+    }
+
+    // get the input file name
+    pAigNew = Ntl_ManScl( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, fLatchConst, fLatchEqual, fVerbose );
+    if ( pAigNew == NULL )
+    {
+        printf( "Abc_CommandAbc8Scl(): 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: *scl [-cevh]\n" );
+    fprintf( stdout, "\t         performs sequential cleanup of the current network\n" );
+    fprintf( stdout, "\t         by removing nodes and latches that do not feed into POs\n" );
+    fprintf( stdout, "\t-c     : sweep stuck-at latches detected by ternary simulation [default = %s]\n", fLatchConst? "yes": "no" );
+    fprintf( stdout, "\t-e     : merge equal latches (same data inputs and init states) [default = %s]\n", fLatchEqual? "yes": "no" );
+    fprintf( stdout, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
 }
 
 /**Function*************************************************************
@@ -16193,7 +16345,92 @@ int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
 ***********************************************************************/
 int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    Aig_Man_t * pAigNew;
+    int c;
+    int nFramesP;
+    int nConfMax;
+    int fVerbose;
+    extern Aig_Man_t * Ntl_ManLcorr( void * p, Aig_Man_t * pAig, int nConfMax, int fVerbose );
+    extern int Ntl_ManIsComb( void * p );
+
+    // set defaults
+    nFramesP   = 0;
+    nConfMax   = 10000;
+    fVerbose   = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PCvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFramesP = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFramesP < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfMax < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Ssw(): There is no design to SAT sweep.\n" );
+        return 1;
+    }
+    if ( pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8Ssw(): There is no AIG to SAT sweep.\n" );
+        return 1;
+    }
+
+    if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
+    {
+        fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
+        return 0;
+    }
+
+    // get the input file name
+    pAigNew = Ntl_ManLcorr( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, nConfMax, fVerbose );
+    if ( pAigNew == NULL )
+    {
+        printf( "Abc_CommandAbc8Ssw(): 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: *lcorr [-C num] [-vh]\n" );
+    fprintf( stdout, "\t         computes latch correspondence using 1-step induction\n" );
+//    fprintf( stdout, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
+    fprintf( stdout, "\t-C num : max conflict number when proving latch equivalence [default = %d]\n", nConfMax );
+    fprintf( stdout, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
 }
 
 /**Function*************************************************************
@@ -16209,7 +16446,184 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
 ***********************************************************************/
 int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    Aig_Man_t * pAigNew;
+    Fra_Ssw_t Pars, * pPars = &Pars;
+    int c;
+    extern Aig_Man_t * Ntl_ManSsw( void * p, Aig_Man_t * pAig, Fra_Ssw_t * pPars );
+    extern int Ntl_ManIsComb( void * p );
+
+    // set defaults
+    pPars->nPartSize  = 0;
+    pPars->nOverSize  = 0;
+    pPars->nFramesP   = 0;
+    pPars->nFramesK   = 1;
+    pPars->nMaxImps   = 5000;
+    pPars->nMaxLevs   = 0;
+    pPars->fUseImps   = 0;
+    pPars->fRewrite   = 0;
+    pPars->fFraiging  = 0;
+    pPars->fLatchCorr = 0;
+    pPars->fWriteImps = 0;
+    pPars->fUse1Hot   = 0;
+    pPars->fVerbose   = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILirfletvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nPartSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nPartSize < 2 ) 
+                goto usage;
+            break;
+        case 'Q':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-Q\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nOverSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nOverSize < 0 ) 
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesP = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesP < 0 ) 
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesK = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesK <= 0 ) 
+                goto usage;
+            break;
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nMaxImps = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nMaxImps <= 0 ) 
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nMaxLevs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nMaxLevs <= 0 ) 
+                goto usage;
+            break;
+        case 'i':
+            pPars->fUseImps ^= 1;
+            break;
+        case 'r':
+            pPars->fRewrite ^= 1;
+            break;
+        case 'f':
+            pPars->fFraiging ^= 1;
+            break;
+        case 'l':
+            pPars->fLatchCorr ^= 1;
+            break;
+        case 'e':
+            pPars->fWriteImps ^= 1;
+            break;
+        case 't':
+            pPars->fUse1Hot ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Ssw(): There is no design to SAT sweep.\n" );
+        return 1;
+    }
+    if ( pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8Ssw(): There is no AIG to SAT sweep.\n" );
+        return 1;
+    }
+
+    if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
+    {
+        fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
+        return 0;
+    }
+
+    if ( pPars->nFramesK > 1 && pPars->fUse1Hot )
+    {
+        printf( "Currrently can only use one-hotness for simple induction (K=1).\n" );
+        return 0;
+    }
+
+    if ( pPars->nFramesP && pPars->fUse1Hot )
+    {
+        printf( "Currrently can only use one-hotness without prefix.\n" );
+        return 0;
+    }
+
+    // get the input file name
+    pAigNew = Ntl_ManSsw( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, pPars );
+    if ( pAigNew == NULL )
+    {
+        printf( "Abc_CommandAbc8Ssw(): 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: *ssw [-PQNFL num] [-lrfetvh]\n" );
+    fprintf( stdout, "\t         performs sequential sweep using K-step induction\n" );
+    fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
+    fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
+    fprintf( stdout, "\t-N num : number of time frames to use as the prefix [default = %d]\n", pPars->nFramesP );
+    fprintf( stdout, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", pPars->nFramesK );
+    fprintf( stdout, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs );
+//    fprintf( stdout, "\t-I num : max number of implications to consider [default = %d]\n", pPars->nMaxImps );
+//    fprintf( stdout, "\t-i     : toggle using implications [default = %s]\n", pPars->fUseImps? "yes": "no" );
+    fprintf( stdout, "\t-l     : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
+    fprintf( stdout, "\t-r     : toggle AIG rewriting [default = %s]\n", pPars->fRewrite? "yes": "no" );
+    fprintf( stdout, "\t-f     : toggle fraiging (combinational SAT sweeping) [default = %s]\n", pPars->fFraiging? "yes": "no" );
+    fprintf( stdout, "\t-e     : toggle writing implications as assertions [default = %s]\n", pPars->fWriteImps? "yes": "no" );
+    fprintf( stdout, "\t-t     : toggle using one-hotness conditions [default = %s]\n", pPars->fUse1Hot? "yes": "no" );
+    fprintf( stdout, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
 }
 
 /**Function*************************************************************
@@ -16225,7 +16639,85 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
 ***********************************************************************/
 int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    Aig_Man_t * pAig;
+    char ** pArgvNew;
+    int nArgcNew;
+    int c;
+    int fRetimeFirst;
+    int fFraiging;
+    int fVerbose;
+    int fVeryVerbose;
+    int nFrames;
+
+    extern int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose );
+    extern Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
+
+    // set defaults
+    nFrames      = 16;
+    fRetimeFirst =  1;
+    fFraiging    =  1;
+    fVerbose     =  0;
+    fVeryVerbose =  0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Krfwvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'r':
+            fRetimeFirst ^= 1;
+            break;
+        case 'f':
+            fFraiging ^= 1;
+            break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
+    if ( nArgcNew != 2 )
+    {
+        printf( "Only works for two designs written from files specified on the command line.\n" );
+        return 1;
+    }
+
+    pAig = Ntl_ManPrepareSec( pArgvNew[0], pArgvNew[1] );
+    Fra_FraigSec( pAig, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose );
+    Aig_ManStop( pAig );
     return 0;
+
+usage:
+    fprintf( stdout, "usage: *dsec [-K num] [-rfwvh] <file1> <file2>\n" );
+    fprintf( stdout, "\t         performs sequential equivalence checking for two designs\n" );
+    fprintf( stdout, "\t-K num : the limit on the depth of induction [default = %d]\n", nFrames );
+    fprintf( stdout, "\t-r     : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
+    fprintf( stdout, "\t-f     : toggles the internal use of fraiging [default = %s]\n", fFraiging? "yes": "no" );
+    fprintf( stdout, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-w     : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    fprintf( stdout, "\tfile1  : the file with the first design\n");
+    fprintf( stdout, "\tfile2  : the file with the second design\n");
+//    fprintf( stdout, "\t         if no files are given, uses the current network and its spec\n");
+//    fprintf( stdout, "\t         if one file is given, uses the current network and the file\n");
+    return 1;
 }
 
 
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 81260e0e..26c64099 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1288,15 +1288,20 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim
 Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
-    Aig_Man_t * pMan;
+    Aig_Man_t * pMan, * pTemp;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return NULL;
-    Aig_ManSeqCleanup( pMan );
-    if ( fLatchConst && pMan->nRegs )
-        pMan = Aig_ManConstReduce( pMan, fVerbose );
-    if ( fLatchEqual && pMan->nRegs )
-        pMan = Aig_ManReduceLaches( pMan, fVerbose );
+//    Aig_ManSeqCleanup( pMan );
+//    if ( fLatchConst && pMan->nRegs )
+//        pMan = Aig_ManConstReduce( pMan, fVerbose );
+//    if ( fLatchEqual && pMan->nRegs )
+//        pMan = Aig_ManReduceLaches( pMan, fVerbose );
+    if ( pMan->vFlopNums )
+        Vec_IntFree( pMan->vFlopNums );
+    pMan->vFlopNums = NULL;
+    pMan = Aig_ManScl( pTemp = pMan, fLatchConst, fLatchEqual, fVerbose );
+    Aig_ManStop( pTemp );
     pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
     Aig_ManStop( pMan );
     return pNtkAig;