Version abc80130_2

1 files changed, 1097 insertions, 99 deletions

diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 39f58a4e..1563bdfe 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -22,16 +22,13 @@
 #include "aig.h"
 #include "dar.h"
 #include "cnf.h"
-//#include "fra.h"
-//#include "fraig.h"
+#include "fra.h"
+#include "fraig.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define Vec_PtrForEachEntryStop( vVec, pEntry, i, Stop )                                     \
-    for ( i = 0; (i < Stop) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -56,6 +53,25 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
     // make sure the latches follow PIs/POs
     if ( fRegisters ) 
     { 
+        assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
+        Abc_NtkForEachCi( pNtk, pObj, i )
+            if ( i < Abc_NtkPiNum(pNtk) )
+            {
+                assert( Abc_ObjIsPi(pObj) );
+                if ( !Abc_ObjIsPi(pObj) )
+                    printf( "Abc_NtkToDar(): Temporary bug: The PI ordering is wrong!\n" );
+            }
+            else
+                assert( Abc_ObjIsBo(pObj) );
+        Abc_NtkForEachCo( pNtk, pObj, i )
+            if ( i < Abc_NtkPoNum(pNtk) )
+            {
+                assert( Abc_ObjIsPo(pObj) );
+                if ( !Abc_ObjIsPo(pObj) )
+                    printf( "Abc_NtkToDar(): Temporary bug: The PO ordering is wrong!\n" );
+            }
+            else
+                assert( Abc_ObjIsBi(pObj) );
         // print warning about initial values
         nDontCares = 0;
         Abc_NtkForEachLatch( pNtk, pObj, i )
@@ -74,7 +90,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
     }
     // create the manager
     pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
-    pMan->pName = util_strsav( pNtk->pName );
+    pMan->pName = Extra_UtilStrsav( pNtk->pName );
     // save the number of registers
     if ( fRegisters )
     {
@@ -83,7 +99,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
         pMan->vFlopNums = NULL;
     }
     // transfer the pointers to the basic nodes
-    Abc_AigConst1(pNtk->pManFunc)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
+    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
     Abc_NtkForEachCi( pNtk, pObj, i )
         pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreatePi(pMan);
     // complement the 1-values registers
@@ -95,8 +111,6 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
 //    pMan->fAddStrash = 1;
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
-        if ( Abc_ObjFaninNum(pObj) == 0 )
-            continue;
         pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
 //        printf( "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
     }
@@ -107,8 +121,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
     // complement the 1-valued registers
     if ( fRegisters )
         Aig_ManForEachLiSeq( pMan, pObjNew, i )
-//            if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) )
-            if ( Abc_LatchIsInit1(Abc_NtkCo(pNtk,i)) )
+            if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) )
                 pObjNew->pFanin0 = Aig_Not(pObjNew->pFanin0);
     // remove dangling nodes
     if ( nNodes = Aig_ManCleanup( pMan ) )
@@ -138,14 +151,14 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
 {
     Vec_Ptr_t * vNodes;
     Abc_Ntk_t * pNtkNew;
-//    Abc_Obj_t * pObjNew;
+    Abc_Obj_t * pObjNew;
     Aig_Obj_t * pObj;
     int i;
 //    assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) );
     // perform strashing
-    pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_TYPE_STRASH, ABC_FUNC_AIG );
+    pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
     // transfer the pointers to the basic nodes
-    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew->pManFunc);
+    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
     Aig_ManForEachPi( pMan, pObj, i )
         pObj->pData = Abc_NtkCi(pNtkNew, i);
     // rebuild the AIG
@@ -163,7 +176,6 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
             break;
         Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
     }
-/*
     // if there are assertions, add them
     if ( pMan->nAsserts > 0 )
         Aig_ManForEachAssert( pMan, pObj, i )
@@ -172,7 +184,6 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
             Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) );
             Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
         }
-*/
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
     return pNtkNew;
@@ -180,30 +191,6 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
 
 /**Function*************************************************************
 
-  Synopsis    [Adds dummy names.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkAddDummyLatchNames( Abc_Ntk_t * pNtk )
-{
-    char Buffer[100];
-    Abc_Obj_t * pObj;
-    int nDigits, i;
-    nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtk) );
-    Abc_NtkForEachLatch( pNtk, pObj, i )
-    {
-        sprintf( Buffer, "L%0*d", nDigits, i );
-        Abc_NtkLogicStoreName( pObj, Buffer );
-    }
-}
-
-/**Function*************************************************************
-
   Synopsis    [Converts the network from the AIG manager into ABC.]
 
   Description [This procedure should be called after seq sweeping, 
@@ -217,38 +204,52 @@ void Abc_NtkAddDummyLatchNames( Abc_Ntk_t * pNtk )
 Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
 {
     Vec_Ptr_t * vNodes;
-    Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObjOld, * pObjNew;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObjNew, * pLatch;
     Aig_Obj_t * pObj, * pObjLo, * pObjLi;
-    int i;
-    // start the network
-    pNtkNew = Abc_NtkAlloc( ABC_TYPE_STRASH, ABC_FUNC_AIG );
-    // duplicate the name and the spec
-    pNtkNew->pName = util_strsav(pNtkOld->pName);
-    pNtkNew->pSpec = util_strsav(pNtkOld->pSpec);
-    // create PIs/POs/latches
-    Abc_NtkForEachPi( pNtkOld, pObjOld, i )
-    {
-        pObjNew = Abc_NtkDupObj( pNtkNew, pObjOld );
-        Abc_NtkLogicStoreName( pObjNew, Abc_ObjName(pObjOld) );
-    }
-    Abc_NtkForEachPo( pNtkOld, pObjOld, i )
+    int i, iNodeId;
+//    assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) );
+    // perform strashing
+    pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // consider the case of target enlargement
+    if ( Abc_NtkCiNum(pNtkNew) < Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan) )
     {
-        pObjNew = Abc_NtkDupObj( pNtkNew, pObjOld );
-        Abc_NtkLogicStoreName( pObjNew, Abc_ObjName(pObjOld) );
+        for ( i = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan) - Abc_NtkCiNum(pNtkNew); i > 0; i-- )
+        {
+            pObjNew = Abc_NtkCreatePi( pNtkNew );
+            Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
+        }
+        Abc_NtkOrderCisCos( pNtkNew );
     }
+    assert( Abc_NtkCiNum(pNtkNew) == Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan) );
+    assert( Abc_NtkCoNum(pNtkNew) == Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) );
+    // transfer the pointers to the basic nodes
+    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
+    Aig_ManForEachPiSeq( pMan, pObj, i )
+        pObj->pData = Abc_NtkCi(pNtkNew, i);
+    // create as many latches as there are registers in the manager
     Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
     {
         pObjNew = Abc_NtkCreateLatch( pNtkNew );
-        Vec_PtrPush( pNtkNew->vCis, pObjNew );
-        Vec_PtrPush( pNtkNew->vCos, pObjNew );
+        pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
+        pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
+        Abc_ObjAddFanin( pObjNew, pObjLi->pData );
+        Abc_ObjAddFanin( pObjLo->pData, pObjNew );
         Abc_LatchSetInit0( pObjNew );
     }
-    Abc_NtkAddDummyLatchNames( pNtkNew );
-    // transfer the pointers to the basic nodes
-    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew->pManFunc);
-    Aig_ManForEachPi( pMan, pObj, i )
-        pObj->pData = Abc_NtkCi(pNtkNew, i);
+    if ( pMan->vFlopNums == NULL )
+        Abc_NtkAddDummyBoxNames( pNtkNew );
+    else
+    {
+        assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) );
+        Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
+        {
+            pLatch = Abc_NtkBox( pNtkOld, Vec_IntEntry( pMan->vFlopNums, i ) );
+            Abc_ObjAssignName( pObjNew, Abc_ObjName(pLatch), NULL );
+            Abc_ObjAssignName( Abc_ObjFanin0(pObjNew),  Abc_ObjName(Abc_ObjFanin0(pLatch)), NULL );
+            Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pLatch)), NULL );
+        }
+    }
     // rebuild the AIG
     vNodes = Aig_ManDfs( pMan );
     Vec_PtrForEachEntry( vNodes, pObj, i )
@@ -260,9 +261,23 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     // connect the PO nodes
     Aig_ManForEachPo( pMan, pObj, i )
     {
-        pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
+        if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts )
+            break;
+        iNodeId = Nm_ManFindIdByNameTwoTypes( pNtkNew->pManName, Abc_ObjName(Abc_NtkCo(pNtkNew, i)), ABC_OBJ_PI, ABC_OBJ_BO );
+        if ( iNodeId >= 0 )
+            pObjNew = Abc_NtkObj( pNtkNew, iNodeId );
+        else
+            pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
         Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
     }
+    // if there are assertions, add them
+    if ( pMan->nAsserts > 0 )
+        Aig_ManForEachAssert( pMan, pObj, i )
+        {
+            pObjNew = Abc_NtkCreateAssert(pNtkNew);
+            Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) );
+            Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
+        }
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
     return pNtkNew;
@@ -288,9 +303,9 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     assert( pMan->pEquivs != NULL );
     assert( Aig_ManBufNum(pMan) == 0 );
     // perform strashing
-    pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_TYPE_STRASH, ABC_FUNC_AIG );
+    pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
     // transfer the pointers to the basic nodes
-    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew->pManFunc);
+    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
     Aig_ManForEachPi( pMan, pObj, i )
         pObj->pData = Abc_NtkCi(pNtkNew, i);
 
@@ -321,6 +336,154 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
 
 /**Function*************************************************************
 
+  Synopsis    [Converts the network from the AIG manager into ABC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
+    Aig_Obj_t * pObj;
+    int i;
+//    assert( Aig_ManLatchNum(pMan) > 0 );
+    // perform strashing
+    pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // transfer the pointers to the basic nodes
+    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
+    Aig_ManForEachPi( pMan, pObj, i )
+        pObj->pData = Abc_NtkPi(pNtkNew, i);
+    // create latches of the new network
+    Aig_ManForEachObj( pMan, pObj, i )
+    {
+        if ( !Aig_ObjIsLatch(pObj) )
+            continue;
+        pObjNew = Abc_NtkCreateLatch( pNtkNew );
+        pFaninNew0 = Abc_NtkCreateBi( pNtkNew );
+        pFaninNew1 = Abc_NtkCreateBo( pNtkNew );
+        Abc_ObjAddFanin( pObjNew, pFaninNew0 );
+        Abc_ObjAddFanin( pFaninNew1, pObjNew );
+        Abc_LatchSetInit0( pObjNew );
+        pObj->pData = Abc_ObjFanout0( pObjNew );
+    }
+    Abc_NtkAddDummyBoxNames( pNtkNew );
+    // rebuild the AIG
+    vNodes = Aig_ManDfs( pMan );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // add the first fanin
+        pObj->pData = pFaninNew0 = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
+        if ( Aig_ObjIsBuf(pObj) )
+            continue;
+        // add the second fanin
+        pFaninNew1 = (Abc_Obj_t *)Aig_ObjChild1Copy(pObj);
+        // create the new node
+        if ( Aig_ObjIsExor(pObj) )
+            pObj->pData = pObjNew = Abc_AigXor( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
+        else
+            pObj->pData = pObjNew = Abc_AigAnd( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
+    }
+    Vec_PtrFree( vNodes );
+    // connect the PO nodes
+    Aig_ManForEachPo( pMan, pObj, i )
+    {
+        pFaninNew = (Abc_Obj_t *)Aig_ObjChild0Copy( pObj );
+        Abc_ObjAddFanin( Abc_NtkPo(pNtkNew, i), pFaninNew );
+    }
+    // connect the latches
+    Aig_ManForEachObj( pMan, pObj, i )
+    {
+        if ( !Aig_ObjIsLatch(pObj) )
+            continue;
+        pFaninNew = (Abc_Obj_t *)Aig_ObjChild0Copy( pObj );
+        Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0(pObj->pData)), pFaninNew );
+    }
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect latch values.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
+{
+    Vec_Int_t * vInits;
+    Abc_Obj_t * pLatch;
+    int i;
+    vInits = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        assert( Abc_LatchIsInit1(pLatch) == 0 );
+        Vec_IntPush( vInits, Abc_LatchIsInit1(pLatch) );
+    }
+    return vInits;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs verification after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
+{
+    int fRemove1, fRemove2;
+    Aig_Man_t * pMan1, * pMan2;
+    int * pArray;
+
+    fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0, 0));
+    fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0, 0));
+
+
+    pMan1 = Abc_NtkToDar( pNtk1, 0 );
+    pMan2 = Abc_NtkToDar( pNtk2, 0 );
+
+    Aig_ManPrintStats( pMan1 );
+    Aig_ManPrintStats( pMan2 );
+
+//    pArray = Abc_NtkGetLatchValues(pNtk1);
+    pArray = NULL;
+    Aig_ManSeqStrash( pMan1, Abc_NtkLatchNum(pNtk1), pArray );
+    free( pArray );
+
+//    pArray = Abc_NtkGetLatchValues(pNtk2);
+    pArray = NULL;
+    Aig_ManSeqStrash( pMan2, Abc_NtkLatchNum(pNtk2), pArray );
+    free( pArray );
+
+    Aig_ManPrintStats( pMan1 );
+    Aig_ManPrintStats( pMan2 );
+
+    Aig_ManStop( pMan1 );
+    Aig_ManStop( pMan2 );
+
+
+    if ( fRemove1 )  Abc_NtkDelete( pNtk1 );
+    if ( fRemove2 )  Abc_NtkDelete( pNtk2 );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Gives the current ABC network to AIG manager for processing.]
 
   Description []
@@ -357,6 +520,7 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
     return pNtkAig;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Gives the current ABC network to AIG manager for processing.]
@@ -368,59 +532,483 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fChoicing, int fVerbose )
 {
+    Fra_Par_t Pars, * pPars = &Pars; 
     Abc_Ntk_t * pNtkAig;
-    Aig_Man_t * pMan;
-    pMan = Abc_NtkToDar( pNtk, 1 );
+    Aig_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
-    Aig_ManSeqCleanup( pMan );
-    if ( fLatchSweep )
+    Fra_ParamsDefault( pPars );
+    pPars->nBTLimitNode = nConfLimit;
+    pPars->fChoicing    = fChoicing;
+    pPars->fDoSparse    = fDoSparse;
+    pPars->fSpeculate   = fSpeculate;
+    pPars->fProve       = fProve;
+    pPars->fVerbose     = fVerbose;
+    pMan = Fra_FraigPerform( pTemp = pMan, pPars );
+    if ( fChoicing )
+        pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
+    else
+        pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    Aig_ManStop( pTemp );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose )
+{
+    extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk, 0 );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose );
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    Aig_ManStop( pTemp );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
+{
+    Aig_Man_t * pMan, * pTemp;
+    Abc_Ntk_t * pNtkAig;
+    int clk;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 0 );
+    if ( pMan == NULL )
+        return NULL;
+//    Aig_ManPrintStats( pMan );
+/*
+//    Aig_ManSupports( pMan );
     {
-        if ( pMan->nRegs )
-            pMan = Aig_ManReduceLaches( pMan, fVerbose );
-        if ( pMan->nRegs )
-            pMan = Aig_ManConstReduce( pMan, fVerbose );
+        Vec_Vec_t * vParts;
+        vParts = Aig_ManPartitionSmart( pMan, 50, 1, NULL );
+        Vec_VecFree( vParts );
     }
-    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+*/
+    Dar_ManRewrite( pMan, pPars );
+//    pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
+//    Aig_ManStop( pTemp );
+
+clk = clock();
+    pMan = Aig_ManDup( pTemp = pMan, 0 ); 
+    Aig_ManStop( pTemp );
+//PRT( "time", clock() - clk );
+
+//    Aig_ManPrintStats( pMan );
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
     Aig_ManStop( pMan );
     return pNtkAig;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Computes latch correspondence.]
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
 
   Description []
                
   SideEffects []
 
   SeeAlso     []
- 
+
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose )
+Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
 {
-    extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter );
     Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
-    pMan = Abc_NtkToDar( pNtk, 1 );
+    int clk;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
-    pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, 0, fVerbose, NULL );
+//    Aig_ManPrintStats( pMan );
+
+    Dar_ManRefactor( pMan, pPars );
+//    pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
+//    Aig_ManStop( pTemp );
+
+clk = clock();
+    pMan = Aig_ManDup( pTemp = pMan, 0 ); 
     Aig_ManStop( pTemp );
-    if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
-        pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+//PRT( "time", clock() - clk );
+
+//    Aig_ManPrintStats( pMan );
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose )
+{
+    Aig_Man_t * pMan, * pTemp;
+    Abc_Ntk_t * pNtkAig;
+    int clk;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 0 );
+    if ( pMan == NULL )
+        return NULL;
+//    Aig_ManPrintStats( pMan );
+
+clk = clock();
+    pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fVerbose ); 
+    Aig_ManStop( pTemp );
+//PRT( "time", clock() - clk );
+
+//    Aig_ManPrintStats( pMan );
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose )
+{
+    Aig_Man_t * pMan, * pTemp;
+    Abc_Ntk_t * pNtkAig;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 0 );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fVerbose );
+    Aig_ManStop( pTemp );
+    pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
+{
+    Aig_Man_t * pMan, * pTemp;
+    Abc_Ntk_t * pNtkAig;
+    int clk;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 0 );
+    if ( pMan == NULL )
+        return NULL;
+//    Aig_ManPrintStats( pMan );
+
+clk = clock();
+    pMan = Dar_ManRwsat( pTemp = pMan, fBalance, fVerbose ); 
+    Aig_ManStop( pTemp );
+//PRT( "time", clock() - clk );
+
+//    Aig_ManPrintStats( pMan );
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t * vMapped )
+{
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pNode, * pNodeNew;
+    Aig_Obj_t * pObj, * pLeaf;
+    Cnf_Cut_t * pCut;
+    Vec_Int_t * vCover;
+    unsigned uTruth;
+    int i, k, nDupGates;
+    // create the new network
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    // make the mapper point to the new network
+    Aig_ManConst1(p->pManAig)->pData = Abc_NtkCreateNodeConst1(pNtkNew);
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        Aig_ManPi(p->pManAig, i)->pData = pNode->pCopy;
+    // process the nodes in topological order
+    vCover = Vec_IntAlloc( 1 << 16 );
+    Vec_PtrForEachEntry( vMapped, pObj, i )
+    {
+        // create new node
+        pNodeNew = Abc_NtkCreateNode( pNtkNew );
+        // add fanins according to the cut
+        pCut = pObj->pData;
+        Cnf_CutForEachLeaf( p->pManAig, pCut, pLeaf, k )
+            Abc_ObjAddFanin( pNodeNew, pLeaf->pData );
+        // add logic function
+        if ( pCut->nFanins < 5 )
+        {
+            uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
+            Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover );
+            pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, vCover );
+        }
+        else
+            pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] );
+        // save the node
+        pObj->pData = pNodeNew;
+    }
+    Vec_IntFree( vCover );
+    // add the CO drivers
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        pObj = Aig_ManPo(p->pManAig, i);
+        pNodeNew = Abc_ObjNotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+        Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
+    }
+
+    // remove the constant node if not used
+    pNodeNew = (Abc_Obj_t *)Aig_ManConst1(p->pManAig)->pData;
+    if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
+        Abc_NtkDeleteObj( pNodeNew );
+    // minimize the node
+//    Abc_NtkSweep( pNtkNew, 0 );
+    // decouple the PO driver nodes to reduce the number of levels
+    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+//    if ( nDupGates && If_ManReadVerbose(pIfMan) )
+//        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkConstructFromCnf(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
+{
+    Vec_Ptr_t * vMapped;
+    Aig_Man_t * pMan;
+    Cnf_Man_t * pManCnf;
+    Cnf_Dat_t * pCnf;
+    Abc_Ntk_t * pNtkNew = NULL;
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    // convert to the AIG manager
+    pMan = Abc_NtkToDar( pNtk, 0 );
+    if ( pMan == NULL )
+        return NULL;
+    if ( !Aig_ManCheck( pMan ) )
+    {
+        printf( "Abc_NtkDarToCnf: AIG check has failed.\n" );
+        Aig_ManStop( pMan );
+        return NULL;
+    }
+    // perform balance
+    Aig_ManPrintStats( pMan );
+
+    // derive CNF
+    pCnf = Cnf_Derive( pMan, 0 );
+    pManCnf = Cnf_ManRead();
+
+    // write the network for verification
+    vMapped = Cnf_ManScanMapping( pManCnf, 1, 0 );
+    pNtkNew = Abc_NtkConstructFromCnf( pNtk, pManCnf, vMapped );
+    Vec_PtrFree( vMapped );
+
+    // write CNF into a file
+    Cnf_DataWriteIntoFile( pCnf, pFileName, 0 );
+    Cnf_DataFree( pCnf );
+    Cnf_ClearMemory();
+
+    Aig_ManStop( pMan );
+    return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Solves combinational miter using a SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose )
+{
+    Aig_Man_t * pMan;
+    int RetValue;//, clk = clock();
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( Abc_NtkLatchNum(pNtk) == 0 );
+    assert( Abc_NtkPoNum(pNtk) == 1 );
+    pMan = Abc_NtkToDar( pNtk, 0 );
+    RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fVerbose ); 
+    pNtk->pModel = pMan->pData, pMan->pData = NULL;
+    Aig_ManStop( pMan );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVerbose )
+{
+    Aig_Man_t * pMan, * pMan1, * pMan2;
+    Abc_Ntk_t * pMiter;
+    int RetValue, clkTotal = clock();
+
+    // cannot partition if it is already a miter
+    if ( pNtk2 == NULL && fPartition == 1 )
+    {
+        printf( "Abc_NtkDarCec(): Switching to non-partitioned CEC for the miter.\n" );
+        fPartition = 0;
+    }
+
+    // if partitioning is selected, call partitioned CEC
+    if ( fPartition )
+    {
+        pMan1 = Abc_NtkToDar( pNtk1, 0 );
+        pMan2 = Abc_NtkToDar( pNtk2, 0 );
+        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, fVerbose );
+        Aig_ManStop( pMan1 );
+        Aig_ManStop( pMan2 );
+        goto finish;
+    }
+
+    if ( pNtk2 != NULL )
+    {
+        // get the miter of the two networks
+        pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
+        if ( pMiter == NULL )
+        {
+            printf( "Miter computation has failed.\n" );
+            return 0;
+        }
+    }
     else
     {
-        Abc_Obj_t * pObj;
-        int i;
-        pNtkAig = Abc_NtkFromDar( pNtk, pMan );
-        Abc_NtkForEachLatch( pNtkAig, pObj, i )
-            Abc_LatchSetInit0( pObj );
+        pMiter = Abc_NtkDup( pNtk1 );
+    }
+    RetValue = Abc_NtkMiterIsConstant( pMiter );
+    if ( RetValue == 0 )
+    {
+//        extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
+        printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
+        // report the error
+        if ( pNtk2 == NULL )
+            pNtk1->pModel = Abc_NtkVerifyGetCleanModel( pNtk1, 1 );
+//        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
+//        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
+//        FREE( pMiter->pModel );
+        Abc_NtkDelete( pMiter );
+        return 0;
     }
+    if ( RetValue == 1 )
+    {
+        Abc_NtkDelete( pMiter );
+        printf( "Networks are equivalent after structural hashing.\n" );
+        return 1;
+    }
+
+    // derive the AIG manager
+    pMan = Abc_NtkToDar( pMiter, 0 );
+    Abc_NtkDelete( pMiter );
+    if ( pMan == NULL )
+    {
+        printf( "Converting miter into AIG has failed.\n" );
+        return -1;
+    }
+    // perform verification
+    RetValue = Fra_FraigCec( &pMan, fVerbose );
+    // transfer model if given
+    if ( pNtk2 == NULL )
+        pNtk1->pModel = pMan->pData, pMan->pData = NULL;
     Aig_ManStop( pMan );
-    return pNtkAig;
+
+finish:
+    // report the miter
+    if ( RetValue == 1 )
+    {
+        printf( "Networks are equivalent.   " );
+PRT( "Time", clock() - clkTotal );
+    }
+    else if ( RetValue == 0 )
+    {
+        printf( "Networks are NOT EQUIVALENT.   " );
+PRT( "Time", clock() - clkTotal );
+    }
+    else
+    {
+        printf( "Networks are UNDECIDED.   " );
+PRT( "Time", clock() - clkTotal );
+    }
+    fflush( stdout );
+    return RetValue;
 }
 
 /**Function*************************************************************
@@ -436,8 +1024,7 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose )
 {
-    extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
-//    Fraig_Params_t Params;
+    Fraig_Params_t Params;
     Abc_Ntk_t * pNtkAig, * pNtkFraig;
     Aig_Man_t * pMan, * pTemp;
     int clk = clock();
@@ -445,8 +1032,8 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, in
     // preprocess the miter by fraiging it
     // (note that for each functional class, fraiging leaves one representative;
     // so fraiging does not reduce the number of functions represented by nodes
-//    Fraig_ParamsSetDefault( &Params );
-//    Params.nBTLimit = 100000;
+    Fraig_ParamsSetDefault( &Params );
+    Params.nBTLimit = 100000;
 //    pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
     pNtkFraig = Abc_NtkDup( pNtk );
 if ( fVerbose ) 
@@ -478,6 +1065,113 @@ PRT( "Initial fraiging time", clock() - clk );
 
 /**Function*************************************************************
 
+  Synopsis    [Computes latch correspondence.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose )
+{
+    Aig_Man_t * pMan, * pTemp;
+    Abc_Ntk_t * pNtkAig;
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, 0, fVerbose, NULL );
+    Aig_ManStop( pTemp );
+    if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
+        pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+    else
+    {
+        Abc_Obj_t * pObj;
+        int i;
+        pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+        Abc_NtkForEachLatch( pNtkAig, pObj, i )
+            Abc_LatchSetInit0( pObj );
+    }
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, int fVerbose )
+{
+    Aig_Man_t * pMan;
+    int clk = clock();
+    // derive the AIG manager
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+    {
+        printf( "Converting miter into AIG has failed.\n" );
+        return -1;
+    }
+    assert( pMan->nRegs > 0 );
+    // perform verification
+    Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose );
+    pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
+    if ( pNtk->pSeqModel )
+    {
+        Fra_Cex_t * pCex = pNtk->pSeqModel;
+        printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace). ", pCex->iPo, pCex->iFrame );
+    }
+    else
+        printf( "No output was asserted after BMC with %d frames. ", nFrames );
+PRT( "Time", clock() - clk );
+    Aig_ManStop( pMan );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose )
+{
+    Aig_Man_t * pMan;
+    int RetValue;
+    // derive the AIG manager
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+    {
+        printf( "Converting miter into AIG has failed.\n" );
+        return -1;
+    }
+    assert( pMan->nRegs > 0 );
+    // perform verification
+    RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
+    pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
+    if ( pNtk->pSeqModel )
+    {
+        Fra_Cex_t * pCex = pNtk->pSeqModel;
+        printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace).\n", pCex->iPo, pCex->iFrame );
+    }
+    Aig_ManStop( pMan );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Gives the current ABC network to AIG manager for processing.]
 
   Description []
@@ -489,14 +1183,13 @@ PRT( "Initial fraiging time", clock() - clk );
 ***********************************************************************/
 int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose )
 {
-    extern int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose );
 //    Fraig_Params_t Params;
     Aig_Man_t * pMan;
     Abc_Ntk_t * pMiter;//, * pTemp;
     int RetValue;
  
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
@@ -507,12 +1200,10 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim
     {
         extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
         printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
-/*
         // report the error
         pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
         Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
         FREE( pMiter->pModel );
-*/
         Abc_NtkDelete( pMiter );
         return 0;
     }
@@ -567,7 +1258,314 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
 
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan;
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    Aig_ManSeqCleanup( pMan );
+    if ( fLatchSweep )
+    {
+        if ( pMan->nRegs )
+            pMan = Aig_ManReduceLaches( pMan, fVerbose );
+        if ( pMan->nRegs )
+            pMan = Aig_ManConstReduce( pMan, fVerbose );
+    }
+    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+        return NULL;
+//    Aig_ManReduceLachesCount( pMan );
+    if ( pMan->vFlopNums )
+        Vec_IntFree( pMan->vFlopNums ); 
+    pMan->vFlopNums = NULL;
+
+    pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, 0 );
+    Aig_ManStop( pTemp );
+
+//    pMan = Aig_ManReduceLaches( pMan, 1 );
+//    pMan = Aig_ManConstReduce( pMan, 1 );
+
+    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+        return NULL;
+//    Aig_ManReduceLachesCount( pMan );
+    if ( pMan->vFlopNums )
+        Vec_IntFree( pMan->vFlopNums ); 
+    pMan->vFlopNums = NULL;
+
+    pMan = Aig_ManRetimeFrontier( pTemp = pMan, nStepsMax );
+    Aig_ManStop( pTemp );
+
+//    pMan = Aig_ManReduceLaches( pMan, 1 );
+//    pMan = Aig_ManConstReduce( pMan, 1 );
+
+    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
+{
+    Aig_Man_t * pMan;
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+        return;
+//    Aig_ManReduceLachesCount( pMan );
+    if ( pMan->vFlopNums )
+        Vec_IntFree( pMan->vFlopNums ); 
+    pMan->vFlopNums = NULL;
+    Aig_ManHaigRecord( pMan );
+    Aig_ManStop( pMan );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs random simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
+{
+    Aig_Man_t * pMan;
+    Fra_Sml_t * pSml;
+    Fra_Cex_t * pCex;
+    int RetValue, clk = clock();
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    pSml = Fra_SmlSimulateSeq( pMan, 0, nFrames, nWords );
+    if ( pSml->fNonConstOut )
+    {
+        pCex = Fra_SmlGetCounterExample( pSml );
+        if ( pCex )
+            printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
+                nFrames, nWords, pCex->iPo, pCex->iFrame );
+        pNtk->pSeqModel = pCex;
+        RetValue = 1;
+    }
+    else
+    {
+        RetValue = 0;
+        printf( "Simulation of %d frames with %d words did not assert the outputs. ", 
+            nFrames, nWords );
+    }
+    PRT( "Time", clock() - clk );
+    Fra_SmlStop( pSml );
+    Aig_ManStop( pMan );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nPref, int nClauses, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose )
+{
+    extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose );
+    extern int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClauses, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose );
+    Aig_Man_t * pMan;
+    if ( fTarget && Abc_NtkPoNum(pNtk) != 1 )
+    {
+        printf( "The number of outputs should be 1.\n" );
+        return 1;
+    }
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+        return 1;
+//    Aig_ManReduceLachesCount( pMan );
+    if ( pMan->vFlopNums )
+        Vec_IntFree( pMan->vFlopNums ); 
+    pMan->vFlopNums = NULL;
+
+//    Fra_Clau( pMan, nStepsMax, fVerbose, fVeryVerbose );
+    Fra_Claus( pMan, nFrames, nPref, nClauses, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fBmc, fRefs, fTarget, fVerbose, fVeryVerbose );
+    Aig_ManStop( pMan );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs targe enlargement.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Aig_ManFrames( pTemp = pMan, nFrames, 0, 1, 1, 1, NULL );
+    Aig_ManStop( pTemp );
+    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Interplates two networks.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
+{
+    extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose );
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pManOn, * pManOff, * pManAig;
+    if ( Abc_NtkCoNum(pNtkOn) != 1 || Abc_NtkCoNum(pNtkOff) != 1 )
+    {
+        printf( "Currently works only for single output networks.\n" );
+        return NULL;
+    }
+    if ( Abc_NtkCiNum(pNtkOn) != Abc_NtkCiNum(pNtkOff) )
+    {
+        printf( "The number of PIs should be the same.\n" );
+        return NULL;
+    }
+    // create internal AIGs
+    pManOn = Abc_NtkToDar( pNtkOn, 0 );
+    if ( pManOn == NULL )
+        return NULL;
+    pManOff = Abc_NtkToDar( pNtkOff, 0 );
+    if ( pManOff == NULL )
+        return NULL;
+    // derive the interpolant
+    pManAig = Aig_ManInter( pManOn, pManOff, fVerbose );
+    if ( pManAig == NULL )
+    {
+        printf( "Interpolant computation failed.\n" );
+        return NULL;
+    }
+    Aig_ManStop( pManOn );
+    Aig_ManStop( pManOff );
+    // create logic network
+    pNtkAig = Abc_NtkFromDar( pNtkOn, pManAig );
+    Aig_ManStop( pManAig );
+    return pNtkAig;
+}
+
+
+#include "ntl.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Performs targe enlargement.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDarTestBlif( char * pFileName )
+{
+    char Buffer[1000];
+    Ntl_Man_t * p;
+    p = Ioa_ReadBlif( pFileName, 1 );
+    if ( p == NULL )
+    {
+        printf( "Abc_NtkDarTestBlif(): Reading BLIF has failed.\n" );
+        return;
+    }
+    Ntl_ManPrintStats( p );
+//    if ( !Ntl_ManInsertTest( p ) )
+    if ( !Ntl_ManInsertTestIf( p ) )
+    {
+        printf( "Abc_NtkDarTestBlif(): Tranformation of the netlist has failed.\n" );
+        return;
+    }
+//    sprintf( Buffer, "%s_.blif", p->pName );
+    sprintf( Buffer, "test_.blif", p->pName );
+    Ioa_WriteBlif( p, Buffer );
+    Ntl_ManFree( p );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///