diff --git a/abclib.dsp b/abclib.dsp
index 9e99fb9462..500ffcaf0b 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3323,47 +3323,47 @@ SOURCE=.\src\opt\fxu\fxuUpdate.c
 # PROP Default_Filter ""
 # Begin Source File
 
-SOURCE=.\src\opt\rar\rewire_map.h
+SOURCE=.\src\opt\rar\rewireMap.h
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\opt\rar\rewire_miaig.h
+SOURCE=.\src\opt\rar\rewireMiaig.h
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\opt\rar\rewire_rar.h
+SOURCE=.\src\opt\rar\rewireRar.h
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\opt\rar\rewire_rng.h
+SOURCE=.\src\opt\rar\rewireRng.h
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\opt\rar\rewire_time.h
+SOURCE=.\src\opt\rar\rewireTime.h
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\opt\rar\rewire_tt.h
+SOURCE=.\src\opt\rar\rewireTt.h
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\opt\rar\rewire_vec.h
+SOURCE=.\src\opt\rar\rewireVec.h
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\opt\rar\rewire_map.c
+SOURCE=.\src\opt\rar\rewireMap.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\opt\rar\rewire_miaig.cpp
+SOURCE=.\src\opt\rar\rewireMiaig.cpp
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\opt\rar\rewire_rar.c
+SOURCE=.\src\opt\rar\rewireRar.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\opt\rar\rewire_rng.c
+SOURCE=.\src\opt\rar\rewireRng.c
 # End Source File
 # End Group
 # Begin Group "rwr"
diff --git a/src/aig/gia/giaStoch.c b/src/aig/gia/giaStoch.c
index 20bfd1d8e3..53e491171e 100644
--- a/src/aig/gia/giaStoch.c
+++ b/src/aig/gia/giaStoch.c
@@ -649,16 +649,31 @@ Gia_Man_t * Gia_ManDupFromArrays( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * v
         pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
     Gia_ManForEachObjVec( vCos, p, pObj, i )
         pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
-    if ( vLevels[0] ) {
+    if ( vLevels[0] && vLevels[1] ) {
         pNew->vCiArrs = Vec_IntAlloc( Gia_ManCiNum(pNew) );
-        Gia_ManForEachObjVec( vCis, p, pObj, i )
-            Vec_IntPush( pNew->vCiArrs, Gia_ObjLevel(p, pObj) );
+        Gia_ManForEachObjVec( vCis, p, pObj, i ) {
+            // Vec_IntPush( pNew->vCiArrs, Gia_ObjLevel(p, pObj) );
+            Vec_IntPush( pNew->vCiArrs, Vec_IntEntry(vLevels[0], Gia_ObjId(p, pObj)) );
+        }
         pNew->vCoReqs = Vec_IntAlloc( Gia_ManCoNum(pNew) );
-        Gia_ManForEachObjVec( vCos, p, pObj, i )
-            Vec_IntPush( pNew->vCoReqs, nLevels - Gia_ObjLevel(p, pObj) );
+        Gia_ManForEachObjVec( vCos, p, pObj, i ) {
+            // Vec_IntPush( pNew->vCoReqs, nLevels - Gia_ObjLevel(p, pObj) );
+            Vec_IntPush( pNew->vCoReqs, nLevels + 1 - Vec_IntEntry(vLevels[1], Gia_ObjId(p, pObj)) );
+            assert( Gia_ObjIsAnd(pObj) );
+        }
     }
     return pNew;
 }
+int Gia_ManLevelR( Gia_Man_t * pMan )
+{
+    int i, LevelMax = Gia_ManLevelRNum( pMan );
+    Gia_Obj_t * pNode;
+    Gia_ManForEachObj( pMan, pNode, i )
+        Gia_ObjSetLevel( pMan, pNode, (int)(LevelMax - Gia_ObjLevel(pMan, pNode) + 1) );
+    Gia_ManForEachCi( pMan, pNode, i )
+        Gia_ObjSetLevel( pMan, pNode, 0 );
+    return LevelMax;
+}
 Vec_Ptr_t * Gia_ManDupWindows( Gia_Man_t * pMan, Vec_Ptr_t * vvIns, Vec_Ptr_t * vvNodes, Vec_Ptr_t * vvOuts, int fDelayOpt )
 {
     // compute direct and reverse level
@@ -669,7 +684,7 @@ Vec_Ptr_t * Gia_ManDupWindows( Gia_Man_t * pMan, Vec_Ptr_t * vvIns, Vec_Ptr_t *
         ABC_SWAP( Vec_Int_t *, vLevels[0], pMan->vLevels );
         Levels[1] = Gia_ManLevelRNum( pMan );
         ABC_SWAP( Vec_Int_t *, vLevels[1], pMan->vLevels );
-        assert( Levels[0] == Levels[1] );
+        assert( (Levels[0] + 1) == Levels[1] ); 
     }    
     Vec_Int_t * vNodes; int i;
     Vec_Ptr_t * vWins = Vec_PtrAlloc( Vec_PtrSize(vvIns) );
@@ -687,16 +702,6 @@ Vec_Ptr_t * Gia_ManDupWindows( Gia_Man_t * pMan, Vec_Ptr_t * vvIns, Vec_Ptr_t *
     Vec_IntFreeP( &vLevels[1] );    
     return vWins;
 }
-int Gia_ManLevelR( Gia_Man_t * pMan )
-{
-    int i, LevelMax = Gia_ManLevelRNum( pMan );
-    Gia_Obj_t * pNode;
-    Gia_ManForEachObj( pMan, pNode, i )
-        Gia_ObjSetLevel( pMan, pNode, (int)(LevelMax - Gia_ObjLevel(pMan, pNode) + 1) );
-    Gia_ManForEachCi( pMan, pNode, i )
-        Gia_ObjSetLevel( pMan, pNode, 0 );
-    return LevelMax;
-}
 Vec_Ptr_t * Gia_ManExtractPartitions( Gia_Man_t * pMan, int Iter, int nSuppMax, Vec_Ptr_t ** pvIns, Vec_Ptr_t ** pvOuts, Vec_Ptr_t ** pvNodes, int fOverlap, int fDelayOpt )
 {
     // if ( Gia_ManCiNum(pMan) <= nSuppMax ) {
@@ -816,7 +821,7 @@ Vec_Ptr_t * Gia_ManDupDivide( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds
         ABC_SWAP( Vec_Int_t *, vLevels[0], p->vLevels );
         Levels[1] = Gia_ManLevelRNum( p );
         ABC_SWAP( Vec_Int_t *, vLevels[1], p->vLevels );
-        assert( Levels[0] == Levels[1] );
+        // assert( Levels[0] == Levels[1] );
     }
     Vec_Ptr_t * vAigs = Vec_PtrAlloc( Vec_WecSize(vCis) );  int i;
     for ( i = 0; i < Vec_WecSize(vCis); i++ )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4d588134d5..aaef7e349c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -20987,17 +20987,17 @@ int Abc_CommandTimeScale( Abc_Frame_t * pAbc, int argc, char ** argv )
 ***********************************************************************/
 int Abc_CommandRewire( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Abc_Ntk_t *Abc_ManRewire(Abc_Ntk_t *pNtk, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose);
+    extern Abc_Ntk_t *Abc_ManRewire(Abc_Ntk_t *pNtk, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fDch, int fTiming, int nSeed, int fCheck, int fVerbose);
     Abc_Ntk_t *pNtk, *pTemp;
     Gia_Man_t *pExc = NULL;
     FILE *pFile = NULL;
-    int c, nIters = 100000, nExpands = 128, nGrowth = 4, nDivs = -1, nFaninMax = 8, nSeed = 1, nTimeOut = 0, nVerbose = 1, nMode = 0, nMappedMode = 0, nDist = 0, fCheck = 0;
+    int c, nIters = 100000, nExpands = 128, nGrowth = 4, nDivs = -1, nFaninMax = 8, nSeed = 1, nTimeOut = 0, nVerbose = 1, nMode = 0, nMappedMode = 0, nDist = 0, fCheck = 0, fDch = 1, fTiming = 0;
     float nLevelGrowRatio = 0;
     Extra_UtilGetoptReset();
 
     pNtk = Abc_FrameReadNtk(pAbc);
 
-    while ( ( c = Extra_UtilGetopt( argc, argv, "IEGDFSTMALRCVch" ) ) != EOF ) {
+    while ( ( c = Extra_UtilGetopt( argc, argv, "IEGDFSTMALRCVdtch" ) ) != EOF ) {
         switch ( c ) {
         case 'I':
             if ( globalUtilOptind >= argc )
@@ -21126,6 +21126,12 @@ int Abc_CommandRewire( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             fCheck ^= 1;
             break;
+        case 'd':
+            fDch ^= 1;
+            break;
+        case 't':
+            fTiming ^= 1;
+            break;
         case 'h':
         default:
             goto usage;
@@ -21143,16 +21149,16 @@ int Abc_CommandRewire( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( nMode == 0 && !Abc_NtkIsStrash(pNtk) )
     {
-        Abc_Print( -1, "Rewiring works only for the AIG representation (run \"strash\").\n" );
+        Abc_Print( -1, "Rewiring operates only on specific network representations. Use \"strash\" to apply it to an AIG, or add the \"-M 1\" flag to enable it for a mapped network.\n" );
         return 1;
     }
-    if ( nMode >= 1 && Abc_FrameReadLibGen2() == NULL )
+    if ( nMode == 1 && Abc_FrameReadLibGen2() == NULL )
     {
         Abc_Print( -1, "Library is not available.\n" );
         return 1;
     }
 
-    pTemp = Abc_ManRewire( pNtk, pExc, nIters, nLevelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, fCheck, nVerbose );
+    pTemp = Abc_ManRewire( pNtk, pExc, nIters, nLevelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, fDch, fTiming, nSeed, fCheck, nVerbose );
     if ( pExc )
         Gia_ManStop( pExc );
     Abc_FrameReplaceCurrentNetwork( pAbc, pTemp );
@@ -21167,13 +21173,15 @@ int Abc_CommandRewire( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Print( -2, "\t-F <num>  :  the limit on the fanin count at a node [default = %d]\n",                    nFaninMax);
     Abc_Print( -2, "\t-L <num>  :  localization distances (0: unlimited) [default = %d]\n",                     nDist);
     Abc_Print( -2, "\t-R <num>  :  level constraint (0: unlimited, 1: preserve level) [default = %g]\n",        nLevelGrowRatio);
-    Abc_Print( -2, "\t-M <num>  :  optimization target [default = %s]\n",                                       nMode ? "area" : "AIG node" );
+    Abc_Print( -2, "\t-M <num>  :  optimization target [default = %s]\n",                                       nMode ? "mapped" : "AIG" );
     Abc_Print( -2, "\t-A <num>  :  mapper (0: amap, 1: &nf, 2: &simap) (experimental) [default = %d]\n",        nMappedMode );
     Abc_Print( -2, "\t-C <file> :  AIGER specifying external cares\n");
     Abc_Print( -2, "\t-S <num>  :  the random seed (0: random, >= 1: user defined) [default = %d]\n",           nSeed );
     Abc_Print( -2, "\t-T <num>  :  the timeout in seconds (0: unlimited) [default = %d]\n",                     nTimeOut );
     Abc_Print( -2, "\t-V <num>  :  the verbosity level [default = %d]\n",                                       nVerbose );
-    Abc_Print( -2, "\t-c        :  check the equivalence [default = %s]\n", fCheck ? "yes" : "no" );
+    Abc_Print( -2, "\t-c        :  check the equivalence [default = %s]\n",                                     fCheck ? "yes" : "no" );
+    Abc_Print( -2, "\t-d        :  toggle perform \"dch\" before mapping [default = %s]\n",                     fDch ? "yes" : "no" );
+    Abc_Print( -2, "\t-t        :  toggle timing-driven rewiring [default = %s]\n",                             fTiming ? "yes" : "no" );
     Abc_Print( -2, "\t-h        :  prints the command usage\n" );
     Abc_Print( -2, "\n\tThis command was contributed by Jiun-Hao Chen from National Taiwan University.\n" );
     return 1;
@@ -46755,14 +46763,14 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
 ***********************************************************************/
 int Abc_CommandAbc9Rewire( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Gia_Man_t *Gia_ManRewire(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fChoices, int fVerbose);
+    extern Gia_Man_t *Gia_ManRewire(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fDch, int fTiming, int nSeed, int fCheck, int fChoices, int fVerbose);
     FILE *pFile = NULL;
     Gia_Man_t *pTemp, *pExc = NULL;
-    int c, nIters = 100000, nExpands = 128, nGrowth = 4, nDivs = -1, nFaninMax = 8, nSeed = 1, nTimeOut = 0, nVerbose = 1, nMode = 0, nMappedMode = 0, nDist = 0, fCheck = 0, fChoices = 0;
+    int c, nIters = 100000, nExpands = 128, nGrowth = 4, nDivs = -1, nFaninMax = 8, nSeed = 1, nTimeOut = 0, nVerbose = 1, nMode = 0, nMappedMode = 0, nDist = 0, fCheck = 0, fChoices = 0, fDch = 1, fTiming = 0;
     float nLevelGrowRatio = 0;
     Extra_UtilGetoptReset();
 
-    while ( ( c = Extra_UtilGetopt( argc, argv, "IEGDFSTMALRCVcsh" ) ) != EOF ) {
+    while ( ( c = Extra_UtilGetopt( argc, argv, "IEGDFSTMALRCVcsdth" ) ) != EOF ) {
         switch ( c ) {
         case 'I':
             if ( globalUtilOptind >= argc )
@@ -46894,6 +46902,12 @@ int Abc_CommandAbc9Rewire( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             fChoices ^= 1;
             break;
+        case 'd':
+            fDch ^= 1;
+            break;
+        case 't':
+            fTiming ^= 1;
+            break;
         case 'h':
         default:
             goto usage;
@@ -46909,13 +46923,13 @@ int Abc_CommandAbc9Rewire( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Empty GIA network.\n" );
         return 1;
     }
-    if ( nMode >= 1 && Abc_FrameReadLibGen2() == NULL )
+    if ( nMode == 1 && Abc_FrameReadLibGen2() == NULL )
     {
         Abc_Print( -1, "Library is not available.\n" );
         return 1;
     }
 
-    pTemp = Gia_ManRewire( pAbc->pGia, pExc, nIters, nLevelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, fCheck, fChoices, nVerbose );
+    pTemp = Gia_ManRewire( pAbc->pGia, pExc, nIters, nLevelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, fDch, fTiming, nSeed, fCheck, fChoices, nVerbose );
     if ( pExc )
         Gia_ManStop( pExc );
     Abc_FrameUpdateGia( pAbc, pTemp );
@@ -46931,14 +46945,16 @@ int Abc_CommandAbc9Rewire( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Print( -2, "\t-F <num>  :  the limit on the fanin count at a node [default = %d]\n",                    nFaninMax);
     Abc_Print( -2, "\t-L <num>  :  localization distances (0: unlimited) [default = %d]\n",                     nDist);
     Abc_Print( -2, "\t-R <num>  :  level constraint (0: unlimited, 1: preserve level) [default = %g]\n",        nLevelGrowRatio);
-    Abc_Print( -2, "\t-M <num>  :  optimization target [default = %s]\n",                                       nMode ? "area" : "AIG node" );
+    Abc_Print( -2, "\t-M <num>  :  optimization target [default = %s]\n",                                       nMode ? "mapped" : "aig" );
     Abc_Print( -2, "\t-A <num>  :  mapper (0: amap, 1: &nf, 2: &simap) (experimental) [default = %d]\n",        nMappedMode );
     Abc_Print( -2, "\t-C <file> :  AIGER specifying external cares\n");
     Abc_Print( -2, "\t-S <num>  :  the random seed (0: random, >= 1: user defined) [default = %d]\n",           nSeed );
     Abc_Print( -2, "\t-T <num>  :  the timeout in seconds (0: unlimited) [default = %d]\n",                     nTimeOut );
     Abc_Print( -2, "\t-V <num>  :  the verbosity level [default = %d]\n",                                       nVerbose );
-    Abc_Print( -2, "\t-c        :  check the equivalence [default = %s]\n", fCheck ? "yes" : "no" );
-    Abc_Print( -2, "\t-s        :  toggle accumulating structural choices [default = %s]\n", fChoices ? "yes" : "no" );
+    Abc_Print( -2, "\t-c        :  check the equivalence [default = %s]\n",                                     fCheck ? "yes" : "no" );
+    Abc_Print( -2, "\t-s        :  toggle accumulating structural choices [default = %s]\n",                    fChoices ? "yes" : "no" );
+    Abc_Print( -2, "\t-d        :  toggle using \"dch\" before mapping [default = %s]\n",                       fDch ? "yes" : "no" );
+    Abc_Print( -2, "\t-t        :  toggle timing-driven re-wiring [default = %s]\n",                            fTiming ? "yes" : "no" );
     Abc_Print( -2, "\t-h        :  prints the command usage\n" );
     Abc_Print( -2, "\n\tThis command was contributed by Jiun-Hao Chen from National Taiwan University.\n" );
     return 1;
diff --git a/src/map/mio/mio.c b/src/map/mio/mio.c
index e06d3f6ea6..3190566453 100644
--- a/src/map/mio/mio.c
+++ b/src/map/mio/mio.c
@@ -77,8 +77,8 @@ static char * pMcncGenlib[] = {
 static char * pAndGenlib[] = {
     "GATE zero    0   O=CONST0;\n",
     "GATE one     0   O=CONST1;\n",
-    "GATE buf     1   O=a;              PIN * NONINV  1 999 1.0 0.0 1.0 0.0\n",
-    "GATE inv     1   O=!a;             PIN * INV     1 999 1.0 0.0 1.0 0.0\n",
+    "GATE buf     1   O=a;              PIN * NONINV  1 999 0.0 0.0 0.0 0.0\n",
+    "GATE inv     1   O=!a;             PIN * INV     1 999 0.0 0.0 0.0 0.0\n",
     "GATE and00   1   O=a*b;            PIN * NONINV  1 999 1.0 0.0 1.0 0.0\n",
     "GATE and01   1   O=a*!b;           PIN * NONINV  1 999 1.0 0.0 1.0 0.0\n",
     "GATE and10   1   O=!a*b;           PIN * NONINV  1 999 1.0 0.0 1.0 0.0\n",
diff --git a/src/opt/rar/module.make b/src/opt/rar/module.make
index 47e9101969..6cf2ecca9c 100644
--- a/src/opt/rar/module.make
+++ b/src/opt/rar/module.make
@@ -1,4 +1,4 @@
-SRC += src/opt/rar/rewire_rng.c \
-       src/opt/rar/rewire_map.c \
-       src/opt/rar/rewire_rar.c \
-       src/opt/rar/rewire_miaig.cpp
\ No newline at end of file
+SRC += src/opt/rar/rewireRng.c \
+       src/opt/rar/rewireMap.c \
+       src/opt/rar/rewireRar.c \
+       src/opt/rar/rewireMiaig.cpp
\ No newline at end of file
diff --git a/src/opt/rar/rewire_map.c b/src/opt/rar/rewireMap.c
similarity index 77%
rename from src/opt/rar/rewire_map.c
rename to src/opt/rar/rewireMap.c
index b63da077b5..515726d15e 100644
--- a/src/opt/rar/rewire_map.c
+++ b/src/opt/rar/rewireMap.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [rewire_map.c]
+  FileName    [rewireMap.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,16 +14,17 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: rewire_map.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: rewireMap.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
-#include "rewire_map.h"
+#include "rewireMap.h"
 
 ABC_NAMESPACE_IMPL_START
 
 extern Abc_Ntk_t *Abc_NtkFromAigPhase(Aig_Man_t *pMan);
 extern Abc_Ntk_t *Abc_NtkDarAmap(Abc_Ntk_t *pNtk, Amap_Par_t *pPars);
+extern Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars );
 extern void *Abc_FrameReadLibGen2();
 extern Vec_Int_t * Abc_NtkWriteMiniMapping( Abc_Ntk_t * pNtk );
 extern void Abc_NtkPrintMiniMapping( int * pArray );
@@ -43,6 +44,28 @@ Abc_Ntk_t *Gia_ManRewirePut(Gia_Man_t *pGia) {
     return pNtk;
 }
 
+Abc_Ntk_t *Abc_ManRewireDch(Abc_Ntk_t *pNtk) {
+    Dch_Pars_t Pars, *pPars = &Pars;
+    Dch_ManSetDefaultParams(pPars);
+    pNtk = Abc_NtkDch(pNtk, pPars);
+    if (pNtk == NULL) {
+        Abc_Print(-1, "Dch compute has failed.\n");
+        return NULL;
+    }
+    return pNtk;
+}
+
+Gia_Man_t *Gia_ManRewireDch(Gia_Man_t *pGia) {
+    Dch_Pars_t Pars, *pPars = &Pars;
+    Dch_ManSetDefaultParams(pPars);
+    pGia = Gia_ManPerformDch( pGia, pPars );
+    if (pGia == NULL) {
+        Abc_Print(-1, "Dch compute has failed.\n");
+        return NULL;
+    }
+    return pGia;
+}
+
 Abc_Ntk_t *Abc_ManRewireMapAmap(Abc_Ntk_t *pNtk) {
     Amap_Par_t Pars, *pPars = &Pars;
     Amap_ManSetDefaultParams(pPars);
@@ -67,6 +90,7 @@ Abc_Ntk_t *Gia_ManRewireMapNf(Gia_Man_t *pGia) {
 }
 
 Abc_Ntk_t *Gia_ManRewireMapSimap(Gia_Man_t *pGia, int nBound, int nBTLimit, int nTimeout) {
+    Abc_Print(-1, "[Warning] Gia_ManRewireMapSimap is SAT-based experimental mode.\n");
     if (!Gia_ManSimpleMapping(pGia, nBound, 0, nBTLimit, nTimeout, 0, 0, 0, NULL)) {
         // Abc_Print(-1, "Mapping has failed.\n");
         return NULL;
diff --git a/src/opt/rar/rewire_map.h b/src/opt/rar/rewireMap.h
similarity index 82%
rename from src/opt/rar/rewire_map.h
rename to src/opt/rar/rewireMap.h
index 7ed31f2430..79627665c7 100644
--- a/src/opt/rar/rewire_map.h
+++ b/src/opt/rar/rewireMap.h
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [rewire_map.h]
+  FileName    [rewireMap.h]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: rewire_map.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: rewireMap.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -24,12 +24,15 @@
 #include "base/abc/abc.h"
 #include "aig/gia/giaAig.h"
 #include "map/amap/amap.h"
+#include "proof/dch/dch.h"
 #include "map/mio/mio.h"
 #include "aig/miniaig/miniaig.h"
 
 ABC_NAMESPACE_HEADER_START
 
 Abc_Ntk_t *Gia_ManRewirePut(Gia_Man_t *pGia);
+Abc_Ntk_t *Abc_ManRewireDch(Abc_Ntk_t *pNtk);
+Gia_Man_t *Gia_ManRewireDch(Gia_Man_t *pGia);
 Abc_Ntk_t *Abc_ManRewireMapAmap(Abc_Ntk_t *pNtk);
 Abc_Ntk_t *Gia_ManRewireMapNf(Gia_Man_t *pGia);
 Abc_Ntk_t *Gia_ManRewireMapSimap(Gia_Man_t *pGia, int nBound, int nBTLimit, int nTimeout);
diff --git a/src/opt/rar/rewire_miaig.cpp b/src/opt/rar/rewireMiaig.cpp
similarity index 71%
rename from src/opt/rar/rewire_miaig.cpp
rename to src/opt/rar/rewireMiaig.cpp
index 5d89dde27a..4de7795443 100644
--- a/src/opt/rar/rewire_miaig.cpp
+++ b/src/opt/rar/rewireMiaig.cpp
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [rewire_miaig.cpp]
+  FileName    [rewireMiaig.cpp]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,12 +14,12 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: rewire_miaig.cpp,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: rewireMiaig.cpp,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
-#include "rewire_rar.h"
-#include "rewire_miaig.h"
+#include "rewireRar.h"
+#include "rewireMiaig.h"
 
 #define USE_OLD_LEVEL_SORTING 0
 
@@ -28,45 +28,71 @@ ABC_NAMESPACE_IMPL_START
 #endif // RW_ABC
 
 #ifdef RW_ABC
-Gia_Man_t *Gia_ManRewireInt(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fChoices, int fVerbose) {
+vi *moveVecToVi(Vec_Int_t *v) {
+    vi *p = (vi *)malloc(sizeof(vi));
+    p->size = Vec_IntSize(v);
+    p->cap = Vec_IntCap(v);
+    p->ptr = Vec_IntArray(v);
+    free(v);
+    return p;
+}
+
+vi *copyVecToVi(Vec_Int_t *v) {
+    vi *p = (vi *)malloc(sizeof(vi));
+    p->size = Vec_IntSize(v);
+    p->cap = Vec_IntCap(v);
+    p->ptr = (int *)malloc(sizeof(int) * p->cap);
+    memcpy(p->ptr, Vec_IntArray(v), sizeof(int) * p->size);
+    return p;
+}
+
+Gia_Man_t *Gia_ManRewireInt(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fDch, int fTiming, int nSeed, int fCheck, int fChoices, int fVerbose) {
     Random_Num(nSeed == 0 ? Abc_Random(0) % 10 : nSeed);
     Gia_ChMan_t *pChMan = fChoices ? Gia_ManDupChoicesStart(pGia) : NULL;
 
+    vi *vCiArrs = (pGia->vCiArrs) ? copyVecToVi(pGia->vCiArrs) : NULL;
+    vi *vCoReqs = (pGia->vCoReqs) ? copyVecToVi(pGia->vCoReqs) : NULL;
+
     assert(Gia_ManCiNum(pGia) <= 58);
     Rewire::Miaig pNtkMiaig(pGia);
     if (pExc)
         pNtkMiaig.setExc(pExc);
-    Rewire::Miaig pNew = pNtkMiaig.rewire(nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, fCheck, pChMan, fVerbose);
+    pNtkMiaig.attachTiming(vCiArrs, vCoReqs);
+    Rewire::Miaig pNew = pNtkMiaig.rewire(nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, fDch, fTiming, fCheck, pChMan, fVerbose);
     pNew.setName(Gia_ManName(pGia));
 
+    if (vCiArrs) Vi_Free(vCiArrs);
+    if (vCoReqs) Vi_Free(vCoReqs);
+
     return pChMan ? Gia_ManDupChoicesFinish(pChMan) : pNew.toGia();
 }
 
-Abc_Ntk_t *Abc_ManRewireInt(Abc_Ntk_t *pNtk, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose) {
+Abc_Ntk_t *Abc_ManRewireInt(Abc_Ntk_t *pNtk, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fDch, int fTiming, int nSeed, int fCheck, int fVerbose) {
     Random_Num(nSeed == 0 ? Abc_Random(0) % 10 : nSeed);
 
     assert(Abc_NtkCiNum(pNtk) <= 58);
     int fMapped = nMode == 1;
+    Vec_Int_t *vMapping = (Abc_NtkHasMapping(pNtk)) ? Abc_ManRewireNtkWriteMiniMapping(pNtk) : NULL;
+    float objectiveValue = (vMapping) ? (fTiming ? Abc_NtkDelayTrace(pNtk, 0, 0, 0) : Abc_NtkGetMappedArea(pNtk)) : 0.0f;
     Rewire::Miaig pNtkMiaig(pNtk);
+    if (vMapping)
+        pNtkMiaig.setMapped(vMapping, objectiveValue);
     if (pExc)
         pNtkMiaig.setExc(pExc);
-    Rewire::Miaig pNew = pNtkMiaig.rewire(nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, fMapped, nMappedMode, nDist, fCheck, NULL, fVerbose);
+    Rewire::Miaig pNew = pNtkMiaig.rewire(nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, fDch, fTiming, fCheck, NULL, fVerbose);
     pNew.setName(Abc_NtkName(pNtk));
-    if (nMode > 0) {
-        pNew.countTransistors(1, nMappedMode);
-    }
 
-    return pNew.toNtk(nMode >= 1);
+    return pNew.toNtk(fMapped);
 }
 
-Mini_Aig_t *MiniAig_ManRewireInt(Mini_Aig_t *pAig, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose) {
+Mini_Aig_t *MiniAig_ManRewireInt(Mini_Aig_t *pAig, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fDch, int fTiming, int nSeed, int fCheck, int fVerbose) {
     Random_Num(nSeed == 0 ? Abc_Random(0) % 10 : nSeed);
 
     assert(Mini_AigPiNum(pAig) <= 58);
     Rewire::Miaig pNtkMiaig(pAig);
     if (pExc)
         pNtkMiaig.setExc(pExc);
-    Rewire::Miaig pNew = pNtkMiaig.rewire(nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, fCheck, NULL, fVerbose);
+    Rewire::Miaig pNew = pNtkMiaig.rewire(nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, fDch, fTiming, fCheck, NULL, fVerbose);
 
     return pNew.toMiniAig();
 }
@@ -94,8 +120,9 @@ void Miaig::create(int nIns, int nOuts, int nObjsAlloc) {
         _data->vOrderF = Vi_Alloc(1000);
         _data->vOrderF2 = Vi_Alloc(1000);
         _data->vTfo = Vi_Alloc(1000);
-        _data->pvFans = (vi *)calloc(sizeof(vi), _data->nObjsAlloc);
+        _data->pvFanins = (vi *)calloc(sizeof(vi), _data->nObjsAlloc);
         _data->pLevel = nullptr;
+        _data->pDist = nullptr;
         _data->pTable = nullptr;
         _data->refcount = 1;
         _refcount = &_data->refcount;
@@ -115,23 +142,66 @@ void Miaig::setName(char *pName) {
     }
 }
 
-void Miaig::print(void) {
-    int i, k, iLit;
-    printf("\nAIG printout:\n");
-    printf("Const0\n");
-    Miaig_ForEachInput(i)
-        printf("Pi%d\n", i);
-    Miaig_ForEachNode(i) {
-        printf("Node%d {", i);
-        Miaig_ForEachObjFanin(i, iLit, k)
-            printf(" %d", iLit);
-        printf(" }\n");
+void Miaig::setMapped(Vec_Int_t *vMapping, float objectiveValue) {
+    if (_data) {
+        if (_data->pNtkMapped) {
+            Vi_Free(_data->pNtkMapped);
+        }
+        _data->pNtkMapped = moveVecToVi(vMapping);
+        _data->objectiveValue = objectiveValue;
     }
-    Miaig_ForEachOutput(i) {
-        printf("Po%d ", i);
+}
+
+void Miaig::printNode(int i) {
+    if (!_data) return;
+    int iLit, k;
+    if (i == 0) {
+        printf("Const0\n");
+    } else if (i <= nIns()) {
+        printf("Pi%d", i);
+        if (!_data->pvFanouts) {
+            printf("\n"); return;
+        }
+        printf(" Fanouts: {");
+        Miaig_ForEachObjFanout(i, iLit, k)
+            printf(" %d", iLit); // this is a variable
+        printf(" }");
+        if (!_data->pRequire) {
+            printf("\n"); return;
+        }
+        printf(" Require: %d\n", objRequire(i));
+    } else if (i < nObjs() - nOuts()) {
+        printf("Node%d Level: %d Fanins: {", i, objLevel(i));
+        Miaig_ForEachObjFanin(i, iLit, k)
+            printf(" %s%d", Rw_LitIsCompl(iLit) ? "~" : "", Rw_Lit2Var(iLit)); // this is a literal
+        printf(" }");
+        if (!_data->pvFanouts) {
+            printf("\n"); return;
+        }
+        printf(" Fanouts: {");
+        Miaig_ForEachObjFanout(i, iLit, k)
+            printf(" %d", iLit); // this is a variable
+        printf(" }");
+        if (!_data->pRequire) {
+            printf("\n"); return;
+        }
+        printf(" Require: %d\n", objRequire(i));
+    } else {
+        printf("Po%d ", i - nObjs() + nOuts());
         Miaig_ForEachObjFanin(i, iLit, k)
-            printf(" %d", iLit);
-        printf("\n");
+            printf(" %s%d", Rw_LitIsCompl(iLit) ? "~" : "", Rw_Lit2Var(iLit));
+        if (!_data->pRequire) {
+            printf("\n"); return;
+        }
+        printf(" Require: %d\n", objRequire(i));
+    }
+}
+
+void Miaig::print(void) {
+    int i;
+    printf("\nAIG printout:\n");
+    Miaig_ForEachObj(i) {
+        printNode(i);
     }
 }
 
@@ -242,15 +312,6 @@ Abc_Ntk_t *Miaig::toNtk(int fMapped) {
     return pNtk;
 }
 
-vi *moveVecToVi(Vec_Int_t *v) {
-    vi *p = (vi *)malloc(sizeof(vi));
-    p->size = Vec_IntSize(v);
-    p->cap = Vec_IntCap(v);
-    p->ptr = Vec_IntArray(v);
-    free(v);
-    return p;
-}
-
 void Miaig::setExc(Gia_Man_t *pExc) {
     int i;
     assert(Gia_ManCiNum(pExc) == nIns());
@@ -271,13 +332,14 @@ void Miaig::setExc(Gia_Man_t *pExc) {
 #endif // RW_ABC
 
 // technology mapping
-float Miaig::countTransistors(int reset, int nMappedMode) {
-    if (!reset && _data->nTransistor) return _data->nTransistor;
+float Miaig::countMappedArea(int reset, int nMappedMode, int fDch) {
+    if (!reset && _data->objectiveValue) return _data->objectiveValue;
 #ifdef RW_ABC
     float area = 0;
     Abc_Ntk_t *pNtkMapped = NULL, *pNtkMappedTemp = NULL;
     if (nMappedMode == 0) {        // amap
         Abc_Ntk_t *pNtk = toNtk();
+        if (fDch) pNtk = Abc_ManRewireDch(pNtk);
         pNtkMapped = Abc_ManRewireMapAmap(pNtk);
         Abc_NtkDelete(pNtk);
     } else if (nMappedMode == 1) { // &nf
@@ -306,7 +368,36 @@ float Miaig::countTransistors(int reset, int nMappedMode) {
     float area = countAnd2(reset, 0);
 #endif // RW_ABC
 
-    return _data->nTransistor = area;
+    return _data->objectiveValue = area;
+}
+
+float Miaig::countMappedDelay(int reset, int nMappedMode, int fDch) {
+    if (!reset && _data->objectiveValue) return _data->objectiveValue;
+#ifdef RW_ABC
+    float delay = 0;
+    Abc_Ntk_t *pNtkMapped = NULL;
+    if (nMappedMode == 0) {        // amap
+        Abc_Ntk_t *pNtk = toNtk();
+        pNtkMapped = Abc_ManRewireMapAmap(pNtk);
+        Abc_NtkDelete(pNtk);
+    } else if (nMappedMode == 1) { // &nf
+        Gia_Man_t *pGia = toGia();
+        pNtkMapped = Gia_ManRewireMapNf(pGia);
+        Gia_ManStop(pGia);
+    } else if (nMappedMode == 2) { // &simap
+        printf("[Warning] The &simap mode is not supported for delay optimization.\n");
+    }
+    if (pNtkMapped) {
+        delay = Abc_NtkDelayTrace(pNtkMapped, 0, 0, 0);
+        Vec_Int_t *vMapping = Abc_ManRewireNtkWriteMiniMapping(pNtkMapped);
+        _data->pNtkMapped = moveVecToVi(vMapping);
+        Abc_NtkDelete(pNtkMapped);
+    }
+#else
+    float delay = countLevel(reset, 0);
+#endif // RW_ABC
+
+    return _data->objectiveValue = delay;
 }
 
 // topological collection
@@ -340,7 +431,7 @@ int Miaig::initializeLevels_rec(int iObj) {
     Miaig_ForEachObjFanin(iObj, iLit, i) {
         level = Abc_MaxInt(initializeLevels_rec(Rw_Lit2Var(iLit)), level);
     }
-    return objLevel(iObj) = level + 1;
+    return objLevel(iObj) = level + objFaninNum(iObj) - 1;
 }
 
 void Miaig::initializeLevels(void) {
@@ -351,14 +442,28 @@ void Miaig::initializeLevels(void) {
     Miaig_ForEachObj(i) {
         objLevel(i) = -1;
     }
-    Miaig_ForEachConstInput(i) {
-        objLevel(i) = 0;
+    objLevel(0) = 0; // const0 is always at level 0
+    Miaig_ForEachInput(i) {
+        objLevel(i) = (_data->vCiArrs) ? Vi_Read(_data->vCiArrs, i - 1) : 0; // modify this from external level if provided
     }
     Miaig_ForEachOutput(i) {
         objLevel(i) = initializeLevels_rec(Rw_Lit2Var(objFanin0(i)));
     }
 }
 
+void Miaig::updateLevels_rec(int iObj) {
+    assert(_data->pLevel);
+    assert(_data->pvFanouts);
+    int i, iLit, level = -1;
+    Miaig_ForEachObjFanin(iObj, iLit, i) {
+        level = Abc_MaxInt(objLevel(Rw_Lit2Var(iLit)), level);
+    }
+    objLevel(iObj) = level + objFaninNum(iObj) - 1;
+    Miaig_ForEachObjFanout(iObj, iLit, i) {
+        updateLevels_rec(iLit); // this is a variable
+    }
+}
+
 // distance computation
 void Miaig::initializeDists(void) {
     if (_data->pDist) return;
@@ -395,30 +500,72 @@ void Miaig::markDistanceN(int iObj, int n) {
     }
 }
 
-void Miaig::markCritical(void) {
+void Miaig::initializeRequire_rec(int iObj) {
+    int i, iLit, requireTime = RW_INT_MAX;
+    if (objIsPo(iObj)) return;
+    Miaig_ForEachObjFanout(iObj, iLit, i) { // this is a variable
+        initializeRequire_rec(iLit);
+    }
+    Miaig_ForEachObjFanout(iObj, iLit, i) { // this is a variable
+        requireTime = Rw_MinInt(objRequire(iLit) - (objFaninNum(iLit) - 1), requireTime);
+    }
+    objRequire(iObj) = requireTime;
+}
+
+void Miaig::initializeRequire(void) {
+    if (_data->pRequire) return;
+    _data->pRequire = (int *)malloc(sizeof(int) * nObjs());
+    memset(_data->pRequire, 0, sizeof(int) * nObjs());
+    
     int iObj;
-    int maxRequire = countLevel(0);
-    nTravIds()++;
-    Miaig_ForEachOutput(iObj) {
-        if (objLevel(iObj) != maxRequire) continue;
-        markCritical_rec(iObj);
+    if (_data->vCoReqs) {
+        Miaig_ForEachOutput(iObj) {
+            objRequire(iObj) = Vi_Read(_data->vCoReqs, iObj - nObjs() + nOuts());
+        }
+    } else {
+        int maxRequireTime = countLevel();
+        Miaig_ForEachOutput(iObj) {
+            objRequire(iObj) = maxRequireTime;
+        }
+    }
+    Miaig_ForEachInput(iObj) {
+        initializeRequire_rec(iObj);
     }
 }
 
-void Miaig::markCritical_rec(int iObj) {
-    objTravId(iObj) = nTravIds();
-    if (objIsPi(iObj)) return;
-    int iLit, k;
-    int maxFaninLevel = objLevel(Rw_Lit2Var(objFanin0(iObj)));
-    Miaig_ForEachObjFaninStart(iObj, iLit, k, 1) {
-        maxFaninLevel = Rw_MaxInt(maxFaninLevel, objLevel(Rw_Lit2Var(iLit)));
+void Miaig::updateRequire_rec(int iObj) {
+    assert(_data->pRequire);
+    assert(_data->pvFanouts);
+    int i, iLit, requireTime = RW_INT_MAX;
+    Miaig_ForEachObjFanout(iObj, iLit, i) { // this is a variable
+        requireTime = Rw_MinInt(objRequire(iLit) - (objFaninNum(iLit) - 1), requireTime);
     }
-    Miaig_ForEachObjFanin(iObj, iLit, k) {
-        if (objLevel(Rw_Lit2Var(iLit)) != maxFaninLevel) continue;
-        markCritical_rec(Rw_Lit2Var(iLit));
+    objRequire(iObj) = requireTime;
+    Miaig_ForEachObjFanin(iObj, iLit, i) {
+        updateRequire_rec(Rw_Lit2Var(iLit));
     }
 }
 
+void Miaig::checkTiming(vi *vCiArrs, vi *vCoReqs) {
+    if (_data->pLevel) free(_data->pLevel), _data->pLevel = nullptr;
+    if (_data->pRequire) free(_data->pRequire), _data->pRequire = nullptr;
+    this->attachTiming(vCiArrs, vCoReqs);
+    initializeLevels();
+    initializeRequire();
+    int iObj;
+    Miaig_ForEachOutput(iObj) {
+        if (objLevel(iObj) > objRequire(iObj)) {
+            printf("Timing error: output %d has arrival %d but require %d.\n", iObj, objLevel(iObj), objRequire(iObj));
+            exit(1);
+        }
+    }
+}
+
+void Miaig::initializeFanouts(void) {
+    if (_data->pvFanouts) return;
+    _data->pvFanouts = (vi *)calloc(sizeof(vi), _data->nObjsAlloc);
+}
+
 // reference counting
 void Miaig::refObj(int iObj) {
     int k, iLit;
@@ -485,9 +632,10 @@ int Miaig::markDfs(void) {
 }
 
 // simple duplicator (optionally removes unused nodes)
-Miaig Miaig::dup(int fRemDangle, int fMapped) {
-    // Miaig pNew = Maig_Alloc(nIns(), nOuts(), nObjs());
+Miaig Miaig::dup(int fRemDangle, int fFanout, int fMapped) {
     Miaig pNew(nIns(), nOuts(), nObjs());
+    pNew.attachTiming(_data->vCiArrs, _data->vCoReqs);
+    if (fFanout) pNew.initializeFanouts();
     memset(_data->pCopy, 0, sizeof(int) * nObjs());
     int i, k, iLit; // obj2obj
     if (fRemDangle)
@@ -502,8 +650,10 @@ Miaig Miaig::dup(int fRemDangle, int fMapped) {
         Miaig_ForEachObjFanin(i, iLit, k)
             pNew.appendFanin(objCopy(i), Rw_Lit2LitV(_data->pCopy, iLit));
     }
-    if (_data->pNtkMapped && fMapped)
+    if (_data->pNtkMapped && fMapped) {
         pNew._data->pNtkMapped = Vi_Dup(_data->pNtkMapped);
+        pNew._data->objectiveValue = _data->objectiveValue;
+    }
     return pNew;
 }
 
@@ -528,6 +678,7 @@ void Miaig::dupDfs_rec(Miaig &pNew, int iObj) {
 
 Miaig Miaig::dupDfs(void) {
     Miaig pNew(nIns(), nOuts(), nObjsAlloc());
+    pNew.attachTiming(_data->vCiArrs, _data->vCoReqs);
     // 1. the array is filled with -1 to distinct visited nodes from unvisited
     memset(_data->pCopy, 0xFF, sizeof(int) * nObjsAlloc());
     int i; // obj2obj
@@ -642,9 +793,10 @@ int Miaig::buildNodeCascade(Miaig &pNew, vi *vFanins, int fCprop, int fStrash) {
     return iLit;
 }
 
-Miaig Miaig::dupStrash(int fCprop, int fStrash, int fCascade) {
+Miaig Miaig::dupStrash(int fCprop, int fStrash, int fCascade, int fFanout) {
     int i, nObjsAlloc = 1 + nIns() + nOuts() + countAnd2();
     Miaig pNew(nIns(), nOuts(), nObjsAlloc);
+    pNew.attachTiming(_data->vCiArrs, _data->vCoReqs);
     memset(_data->pCopy, 0, sizeof(int) * nObjs()); // obj2lit
     if (fStrash) {
         assert(pNew._data->pTable == NULL);
@@ -662,7 +814,7 @@ Miaig Miaig::dupStrash(int fCprop, int fStrash, int fCascade) {
     }
     Miaig_ForEachOutput(i)
         pNew.appendFanin(pNew.appendObj(), Rw_Lit2LitL(_data->pCopy, objFanin0(i)));
-    return pNew.dup(1);
+    return pNew.dup(1, fFanout, 0);
 }
 
 // this duplicator converts two-input-node AIG into multi-input-node AIG
@@ -692,12 +844,14 @@ void Miaig::collectSuper_rec(int iLit, int *pStop, vi *vSuper) {
     }
 }
 
-Miaig Miaig::dupMulti(int nFaninMax_, int nGrowth) {
+Miaig Miaig::dupMulti(int nFaninMax, int nGrowth) {
     Miaig pNew(nIns(), nOuts(), nObjs());
+    pNew.attachTiming(_data->vCiArrs, _data->vCoReqs);
+    pNew.initializeFanouts();
     int *pStop = createStops();
     int i, k, iLit;
     vi *vArray = Vi_Alloc(100);
-    assert(nFaninMax_ >= 2 && nGrowth >= 1);
+    assert(nFaninMax >= 2 && nGrowth >= 1);
     memset(_data->pCopy, 0, sizeof(int) * nObjs()); // obj2lit
     Miaig_ForEachConstInput(i)
         objCopy(i) = Rw_Var2Lit(i, 0);
@@ -714,9 +868,9 @@ Miaig Miaig::dupMulti(int nFaninMax_, int nGrowth) {
         if (Vi_Size(vArray) == 1)
             objCopy(i) = Vi_Read(vArray, 0);
         else {
-            int nFaninMaxLocal = 2 + (Random_Num(0) % (nFaninMax_ - 1));
+            int nFaninMaxLocal = 2 + (Random_Num(0) % (nFaninMax - 1));
             int nGrowthLocal = 1 + (Random_Num(0) % nGrowth);
-            assert(nFaninMaxLocal >= 2 && nFaninMaxLocal <= nFaninMax_);
+            assert(nFaninMaxLocal >= 2 && nFaninMaxLocal <= nFaninMax);
             assert(nGrowthLocal >= 1 && nGrowthLocal <= nGrowth);
 
             if (Vi_Size(vArray) > nFaninMaxLocal)
@@ -754,6 +908,29 @@ Miaig Miaig::dupMulti(int nFaninMax_, int nGrowth) {
     return pNew;
 }
 
+Miaig Miaig::dupExtend(int nFaninMax, int nGrowth) {
+    Miaig pNew(nIns(), nOuts(), nObjs());
+    pNew.attachTiming(_data->vCiArrs, _data->vCoReqs);
+    pNew.initializeFanouts();
+    memset(_data->pCopy, 0, sizeof(int) * nObjs());
+    int iObj, k, iLit; // obj2obj
+    Miaig_ForEachInput(iObj)
+        objCopy(iObj) = iObj;
+    Miaig_ForEachNodeOutput(iObj) {
+        int nFaninMaxLocal = 2 + (Random_Num(0) % (nFaninMax - 1));
+        int nGrowthLocal = 1 + (Random_Num(0) % nGrowth);
+        assert(objFaninNum(iObj) > 0);
+        objCopy(iObj) = pNew.appendObj();
+        vi *vFanins = pNew.objFanins(iObj);
+        assert(vFanins->ptr == NULL);
+        vFanins->cap = nFaninMaxLocal + nGrowthLocal;
+        vFanins->ptr = (int *)malloc(sizeof(int) * vFanins->cap);
+        Miaig_ForEachObjFanin(iObj, iLit, k)
+            pNew.appendFanin(objCopy(iObj), Rw_Lit2LitV(_data->pCopy, iLit));
+    }
+    return pNew;
+}
+
 // compute truth table of the node
 void Miaig::truthSimNode(int i) {
     int k, iLit;
@@ -965,9 +1142,9 @@ int Miaig::findShared(int nNewNodesMax) {
     if (nObjs() + nNewNodesMax > nObjsAlloc()) {
         nObjsAlloc() = nObjs() + nNewNodesMax;
         _data->pCopy = (int *)realloc((void *)_data->pCopy, sizeof(int) * nObjsAlloc());
-        _data->pvFans = (vi *)realloc((void *)_data->pvFans, sizeof(vi) * nObjsAlloc());
+        _data->pvFanins = (vi *)realloc((void *)_data->pvFanins, sizeof(vi) * nObjsAlloc());
         memset(_data->pCopy + nObjs(), 0, sizeof(int) * (nObjsAlloc() - nObjs()));
-        memset(_data->pvFans + nObjs(), 0, sizeof(vi) * (nObjsAlloc() - nObjs()));
+        memset(_data->pvFanins + nObjs(), 0, sizeof(vi) * (nObjsAlloc() - nObjs()));
     }
     assert(sizeof(word) == 8);
     int i, nWords = (2 * nObjsAlloc() + 63) / 64; // how many words are needed to have a bitstring with one bit for each literal
@@ -992,8 +1169,14 @@ int Miaig::findShared(int nNewNodesMax) {
 
 int Miaig::checkConst(int iObj, word *pCare, word *pExc, int fCheck, int fVerbose) {
     word *pFunc = objTruth(iObj, 0);
+    int iLit, i;
     if (!Tt_IntersectC(pCare, pFunc, 0, nWords())) {
         derefObj_rec(iObj, -1);
+        if (_data->pvFanouts) {
+            Miaig_ForEachObjFanin(iObj, iLit, i) {
+                Vi_Remove(objFanouts(Rw_Lit2Var(iLit)), iObj);
+            }
+        }
         Vi_Fill(objFanins(iObj), 1, 0); // const0
         refObj(iObj);
         truthUpdate(_data->vTfo, pExc, fCheck);
@@ -1002,6 +1185,11 @@ int Miaig::checkConst(int iObj, word *pCare, word *pExc, int fCheck, int fVerbos
     }
     if (!Tt_IntersectC(pCare, pFunc, 1, nWords())) {
         derefObj_rec(iObj, -1);
+        if (_data->pvFanouts) {
+            Miaig_ForEachObjFanin(iObj, iLit, i) {
+                Vi_Remove(objFanouts(Rw_Lit2Var(iLit)), iObj);
+            }
+        }
         Vi_Fill(objFanins(iObj), 1, 1); // const1
         refObj(iObj);
         truthUpdate(_data->vTfo, pExc, fCheck);
@@ -1011,7 +1199,49 @@ int Miaig::checkConst(int iObj, word *pCare, word *pExc, int fCheck, int fVerbos
     return 0;
 }
 
-int Miaig::expandOne(int iObj, int nAddedMax, int nDist, int nExpandableLevel, word *pExc, int fCheck, int fVerbose) {
+void Miaig::expandOneHeuristicSort(int *pOrderF, int fTiming) {
+    std::stable_sort(pOrderF, pOrderF + Vi_Size(_data->vOrderF), [&](int a, int b) {
+        return objLevel(Rw_Lit2Var(a)) > objLevel(Rw_Lit2Var(b));
+    });
+#if USE_OLD_LEVEL_SORTING
+    std::stable_sort(pOrderF, pOrderF + Vi_Size(_data->vOrderF), [&](int a, int b) {
+        if (objLevel(Rw_Lit2Var(a)) == 0 || objLevel(Rw_Lit2Var(b)) == 0) {
+            return false;
+        }
+        return objRef(Rw_Lit2Var(a)) < objRef(Rw_Lit2Var(b));
+    });
+#else
+    // Sort all literals by objRef except in the case where they refer to a variable on level zero.
+    // Level zero literals are always sorted before non-level zero literals. Two level zero literals are ordered by their
+    // objRef to maintain strict weak ordering.
+    std::stable_sort(pOrderF, pOrderF + Vi_Size(_data->vOrderF), [&](int a, int b) {
+        bool a_is_level_0 = (objLevel(Rw_Lit2Var(a)) == 0);
+        bool b_is_level_0 = (objLevel(Rw_Lit2Var(b)) == 0);
+
+        // Always sort level 0 literals before the rest.
+        if (a_is_level_0 && !b_is_level_0) {
+            return true; // a (level 0) comes before b (non-level 0)
+        }
+        if (!a_is_level_0 && b_is_level_0) {
+            return false; // b (level 0) comes before a (non-level 0)
+        }        
+
+        // If both are level 0 or none are level 0, then sort by objRef. 
+        // If both are level 0 the relative ordering (probably?) doesn't matter, 
+        // so we can just order them anyway by objRef such that we maintain the strict weak ordering.
+        return objRef(Rw_Lit2Var(a)) < objRef(Rw_Lit2Var(b));
+    });
+#endif
+    if (fTiming) {
+        std::stable_sort(pOrderF, pOrderF + Vi_Size(_data->vOrderF), [&](int a, int b) {
+            return (objRequire(Rw_Lit2Var(a)) - objLevel(Rw_Lit2Var(a))) > (objRequire(Rw_Lit2Var(b)) - objLevel(Rw_Lit2Var(b)));
+        });
+    }
+
+}
+
+int Miaig::expandOne(int iObj, int nAddedMax, int nDist, int nExpandableLevel, word *pExc, int fTiming, int fCheck, int fVerbose) {
+    if (fTiming && objRequire(iObj) - objLevel(iObj) < 0) return 0; // skip nodes with slack violations
     int i, k, n, iLit, nAdded = 0;
     word *pCare = computeCareSet(iObj, pExc);
     assert(nAddedMax > 0);
@@ -1033,43 +1263,12 @@ int Miaig::expandOne(int iObj, int nAddedMax, int nDist, int nExpandableLevel, w
     }
     Vi_Randomize(_data->vOrderF);
 
-    int *pOrderF = Vi_Array(_data->vOrderF);
-    std::stable_sort(pOrderF, pOrderF + Vi_Size(_data->vOrderF), [&](int a, int b) {
-        return objLevel(Rw_Lit2Var(a)) > objLevel(Rw_Lit2Var(b));
-    });
-#if USE_OLD_LEVEL_SORTING
-    std::stable_sort(pOrderF, pOrderF + Vi_Size(_data->vOrderF), [&](int a, int b) {
-        if (objLevel(Rw_Lit2Var(a)) == 0 || objLevel(Rw_Lit2Var(b)) == 0) {
-            return false;
-        }
-        return objRef(Rw_Lit2Var(a)) < objRef(Rw_Lit2Var(b));
-    });
-#else
-   // Sort all literals by objRef except in the case where they refer to a variable on level zero.
-   // Level zero literals are always sorted before non-level zero literals. Two level zero literals are ordered by their
-   // objRef to maintain strict weak ordering.
-    std::stable_sort(pOrderF, pOrderF + Vi_Size(_data->vOrderF), [&](int a, int b) {
-     bool a_is_level_0 = (objLevel(Rw_Lit2Var(a)) == 0);
-     bool b_is_level_0 = (objLevel(Rw_Lit2Var(b)) == 0);
-
-     // Always sort level 0 literals before the rest.
-     if (a_is_level_0 && !b_is_level_0) {
-         return true; // a (level 0) comes before b (non-level 0)
-     }
-     if (!a_is_level_0 && b_is_level_0) {
-         return false; // b (level 0) comes before a (non-level 0)
-     }        
-
-     // If both are level 0 or none are level 0, then sort by objRef. 
-     // If both are level 0 the relative ordering (probably?) doesn't matter, 
-     // so we can just order them anyway by objRef such that we maintain the strict weak ordering.
-     return objRef(Rw_Lit2Var(a)) < objRef(Rw_Lit2Var(b));
-    });
-#endif
+    this->expandOneHeuristicSort(Vi_Array(_data->vOrderF), fTiming);
 
     // iterate through candidate fanins (nodes that are not in the TFO of iObj)
     Vi_ForEachEntry(_data->vOrderF, i, k) {
         assert(objTravId(i) != nTravIds());
+        if (fTiming && Rw_MaxInt(objLevel(iObj), objLevel(i)) + objFaninNum(iObj) > objRequire(iObj)) continue;
         // new fanin can be added if its offset does not intersect with the node's onset
         for (n = 0; n < 2; n++)
             if (!Tt_IntersectC(pOnset, objTruth(i, 0), !n, nWords())) {
@@ -1077,18 +1276,59 @@ int Miaig::expandOne(int iObj, int nAddedMax, int nDist, int nExpandableLevel, w
                 appendFanin(iObj, Rw_Var2Lit(i, n));
                 objRef(i)++;
                 nAdded++;
+                if (fTiming) {
+                    updateLevels_rec(iObj); 
+                    updateRequire_rec(iObj);
+                    // checkTiming(_data->vCiArrs, _data->vCoReqs);
+                }
                 break;
             }
         if (nAdded == nAddedMax)
             break;
     }
-    //printf( "Updating TFO of node %d:  ", iObj );  Vi_Print(_data->vTfo);
     truthUpdate(_data->vTfo, pExc, fCheck);
     //assert( objFaninNum(iObj) <= nFaninMax );
     return nAdded;
 }
 
-int Miaig::reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic, word *pExc, int fCheck, int fVerbose) {
+void Miaig::reduceOneHeuristicSort(int *pOrderF, int fTiming) {
+    std::stable_sort(pOrderF, pOrderF + Vi_Size(_data->vOrderF), [&](int a, int b) {
+        return objLevel(Rw_Lit2Var(a)) < objLevel(Rw_Lit2Var(b));
+    });
+#if USE_OLD_LEVEL_SORTING
+    std::stable_sort(pOrderF, pOrderF + Vi_Size(_data->vOrderF), [&](int a, int b) {
+        if (objLevel(Rw_Lit2Var(a)) == 0 || objLevel(Rw_Lit2Var(b)) == 0) {
+            return false;
+        }
+        return objRef(Rw_Lit2Var(a)) > objRef(Rw_Lit2Var(b));
+    });
+#else
+    // Sort all literals by objRef except in the case where they refer to a variable on level zero.
+    // Level zero literals are always sorted before non-level zero literals. Two level zero literals are ordered by their
+    // objRef to maintain strict weak ordering.
+    std::stable_sort(pOrderF, pOrderF + Vi_Size(_data->vOrderF), [&](int a, int b) {
+        bool a_is_level_0 = (objLevel(Rw_Lit2Var(a)) == 0);
+        bool b_is_level_0 = (objLevel(Rw_Lit2Var(b)) == 0);
+
+        // Always sort level 0 literals before the rest.
+        if (a_is_level_0 && !b_is_level_0) {
+            return true; // a (level 0) comes before b (non-level 0)
+        }
+        if (!a_is_level_0 && b_is_level_0) {
+            return false; // b (level 0) comes before a (non-level 0)
+        }        
+
+        // If both are level 0 or none are level 0, then sort by objRef. 
+        // If both are level 0 the relative ordering (probably?) doesn't matter, 
+        // so we can just order them anyway by objRef such that we maintain the strict weak ordering.
+        return objRef(Rw_Lit2Var(a)) < objRef(Rw_Lit2Var(b));
+    });
+#endif
+    // if (fTiming) {
+    // }
+}
+
+int Miaig::reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic, word *pExc, int fTiming, int fCheck, int fVerbose) {
     int n, k, iLit, nFans = objFaninNum(iObj);
     word *pCare = computeCareSet(iObj, pExc);
     if (checkConst(iObj, pCare, pExc, fCheck, fVerbose))
@@ -1102,9 +1342,7 @@ int Miaig::reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic,
     Miaig_ForEachObjFanin(iObj, iLit, k) {
         Tt_DupC(_data->pProd, objTruth(Rw_Lit2Var(iLit), 0), Rw_LitIsCompl(iLit), nWords());
         if (Tt_EqualOnCare(pCare, pFunc, _data->pProd, nWords())) {
-            derefObj(iObj);
-            Vi_Fill(objFanins(iObj), 1, iLit);
-            refObj(iObj);
+            setFanin(iObj, iLit);
             truthUpdate(_data->vTfo, pExc, fCheck);
             if (fVerbose) printf("Reducing node %d fanin count from %d to %d.\n", iObj, nFans, objFaninNum(iObj));
             return nFans - 1;
@@ -1118,40 +1356,7 @@ int Miaig::reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic,
     Vi_Randomize(_data->vOrderF);
 
     if (fHeuristic) {
-        int *pOrderF = Vi_Array(_data->vOrderF);
-        std::stable_sort(pOrderF, pOrderF + Vi_Size(_data->vOrderF), [&](int a, int b) {
-            return objLevel(Rw_Lit2Var(a)) < objLevel(Rw_Lit2Var(b));
-        });
-#if USE_OLD_LEVEL_SORTING
-        std::stable_sort(pOrderF, pOrderF + Vi_Size(_data->vOrderF), [&](int a, int b) {
-            if (objLevel(Rw_Lit2Var(a)) == 0 || objLevel(Rw_Lit2Var(b)) == 0) {
-                return false;
-            }
-            return objRef(Rw_Lit2Var(a)) > objRef(Rw_Lit2Var(b));
-        });
-#else
-   // Sort all literals by objRef except in the case where they refer to a variable on level zero.
-   // Level zero literals are always sorted before non-level zero literals. Two level zero literals are ordered by their
-   // objRef to maintain strict weak ordering.
-    std::stable_sort(pOrderF, pOrderF + Vi_Size(_data->vOrderF), [&](int a, int b) {
-     bool a_is_level_0 = (objLevel(Rw_Lit2Var(a)) == 0);
-     bool b_is_level_0 = (objLevel(Rw_Lit2Var(b)) == 0);
-
-     // Always sort level 0 literals before the rest.
-     if (a_is_level_0 && !b_is_level_0) {
-         return true; // a (level 0) comes before b (non-level 0)
-     }
-     if (!a_is_level_0 && b_is_level_0) {
-         return false; // b (level 0) comes before a (non-level 0)
-     }        
-
-     // If both are level 0 or none are level 0, then sort by objRef. 
-     // If both are level 0 the relative ordering (probably?) doesn't matter, 
-     // so we can just order them anyway by objRef such that we maintain the strict weak ordering.
-     return objRef(Rw_Lit2Var(a)) < objRef(Rw_Lit2Var(b));
-    });
-#endif
-
+        this->reduceOneHeuristicSort(Vi_Array(_data->vOrderF), fTiming);
     }
 
     assert(Vi_Size(_data->vOrderF) == nFans);
@@ -1166,9 +1371,19 @@ int Miaig::reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic,
     // update the node if it is reduced
     if (Vi_Size(_data->vOrderF) < nFans) {
         derefObj(iObj);
+        if (_data->pvFanouts) {
+            int iLit2, i;
+            Miaig_ForEachObjFanin(iObj, iLit2, i) {
+                Vi_Remove(objFanouts(Rw_Lit2Var(iLit2)), iObj);
+            }
+        }
         Vi_Shrink(objFanins(iObj), 0);
-        Vi_ForEachEntry(_data->vOrderF, iLit, k)
+        Vi_ForEachEntry(_data->vOrderF, iLit, k) {
+            if (_data->pvFanouts) {
+                Vi_PushOrder(objFanouts(Rw_Lit2Var(iLit)), iObj);
+            }
             Vi_PushOrder(objFanins(iObj), iLit);
+        }
         refObj(iObj);
         truthUpdate(_data->vTfo, pExc, fCheck);
         if (fVerbose) printf("Reducing node %d fanin count from %d to %d.\n", iObj, nFans, objFaninNum(iObj));
@@ -1177,9 +1392,9 @@ int Miaig::reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic,
     return 0;
 }
 
-int Miaig::expandThenReduceOne(int iNode, int nFaninAddLimit, int nDist, int nExpandableLevel, word *pExc, int fCheck, int fVerbose) {
-    expandOne(iNode, std::min(Vi_Space(objFanins(iNode)), nFaninAddLimit), nDist, nExpandableLevel, pExc, fCheck, fVerbose);
-    reduceOne(iNode, 0, 0, 0, pExc, fCheck, fVerbose);
+int Miaig::expandThenReduceOne(int iNode, int nFaninAddLimit, int nDist, int nExpandableLevel, word *pExc, int fTiming, int fCheck, int fVerbose) {
+    expandOne(iNode, std::min(Vi_Space(objFanins(iNode)), nFaninAddLimit), nDist, nExpandableLevel, pExc, fTiming, fCheck, fVerbose);
+    reduceOne(iNode, 0, 0, 0, pExc, fTiming, fCheck, fVerbose);
     return 0;
 }
 
@@ -1192,7 +1407,7 @@ vi *Miaig::createRandomOrder(void) {
     return _data->vOrder;
 }
 
-Miaig Miaig::expand(int nFaninAddLimitAll, int nDist, int nExpandableLevel, word *pExc, int fCheck, int fVerbose) {
+Miaig Miaig::expand(int nFaninAddLimitAll, int nDist, int nExpandableLevel, word *pExc, int fTiming, int fCheck, int fVerbose) {
     int i, iNode, nAdded = 0;
     assert(nFaninAddLimitAll > 0);
     vi *vOrder = createRandomOrder();
@@ -1201,8 +1416,9 @@ Miaig Miaig::expand(int nFaninAddLimitAll, int nDist, int nExpandableLevel, word
     initializeRefs();
     initializeLevels();
     if (nDist) initializeDists();
+    if (fTiming) initializeRequire();
     Vi_ForEachEntry(vOrder, iNode, i) {
-        nAdded += expandOne(iNode, std::min(Vi_Space(objFanins(iNode)), nFaninAddLimitAll - nAdded), nDist, nExpandableLevel, pExc, fCheck, fVerbose);
+        nAdded += expandOne(iNode, std::min(Vi_Space(objFanins(iNode)), nFaninAddLimitAll - nAdded), nDist, nExpandableLevel, pExc, fTiming, fCheck, fVerbose);
         if (nAdded >= nFaninAddLimitAll)
             break;
     }
@@ -1213,7 +1429,7 @@ Miaig Miaig::expand(int nFaninAddLimitAll, int nDist, int nExpandableLevel, word
 
 // perform shared logic extraction
 Miaig Miaig::share(int nNewNodesMax) {
-    Miaig pCopy = dup(0);
+    Miaig pCopy = dup(0, 0, 0);
     int nNewNodes = pCopy.findShared(nNewNodesMax);
     if (nNewNodes == 0)
         return pCopy;
@@ -1224,7 +1440,7 @@ Miaig Miaig::share(int nNewNodesMax) {
     return pNew;
 }
 
-Miaig Miaig::reduce(word *pExc, int fCheck, int fVerbose) {
+Miaig Miaig::reduce(word *pExc, int fTiming, int fCheck, int fVerbose) {
     int i, iNode;
     vi *vOrder = topoCollect();
 
@@ -1233,13 +1449,12 @@ Miaig Miaig::reduce(word *pExc, int fCheck, int fVerbose) {
     initializeLevels();
     // works best for final
     Vi_ForEachEntry(vOrder, iNode, i)
-        reduceOne(iNode, 0, 0, 1, pExc, fCheck, fVerbose);
+        reduceOne(iNode, 0, 0, 1, pExc, fTiming, fCheck, fVerbose);
     if (fCheck) verifyRefs();
-    return dupStrash(1, 1, 1);
+    return dupStrash(1, 1, !fTiming);
 }
 
-Miaig Miaig::expandThenReduce(int nFaninAddLimit, int nDist, int nExpandableLevel, word *pExc, int fCheck, int fVerbose) {
-    Miaig pTemp;
+Miaig Miaig::expandThenReduce(int nFaninAddLimit, int nDist, int nExpandableLevel, word *pExc, int fTiming, int fCheck, int fVerbose) {
     int i, iNode;
     vi *vOrder = topoCollect();
 
@@ -1247,20 +1462,21 @@ Miaig Miaig::expandThenReduce(int nFaninAddLimit, int nDist, int nExpandableLeve
     initializeRefs();
     initializeLevels();
     if (nDist) initializeDists();
+    if (fTiming) initializeRequire();
     Vi_ForEachEntry(vOrder, iNode, i) {
-        expandThenReduceOne(iNode, nFaninAddLimit, nDist, nExpandableLevel, pExc, fCheck, fVerbose);
+        expandThenReduceOne(iNode, nFaninAddLimit, nDist, nExpandableLevel, pExc, fTiming, fCheck, fVerbose);
     }
     if (fCheck) verifyRefs();
-    return dupDfs().dupStrash(1, 1, 1);
+    return dupDfs().dupStrash(1, 1, !fTiming, 1);
 }
 
-Miaig Miaig::expandShareReduce(int nFaninAddLimitAll, int nDivs, int nDist, int nExpandableLevel, word *pExc, int fCheck, int nVerbose) {
+Miaig Miaig::expandShareReduce(int nFaninAddLimitAll, int nDivs, int nDist, int nExpandableLevel, word *pExc, int fTiming, int fCheck, int nVerbose) {
     // expand
-    Miaig pNew = expand(nFaninAddLimitAll, nDist, nExpandableLevel, pExc, fCheck, nVerbose);
+    Miaig pNew = expand(nFaninAddLimitAll, nDist, nExpandableLevel, pExc, fTiming, fCheck, nVerbose);
     // share
     pNew = pNew.share(nDivs == -1 ? pNew.nObjs() : nDivs);
     // reduce
-    pNew = pNew.reduce(pExc, fCheck, nVerbose);
+    pNew = pNew.reduce(pExc, fTiming, fCheck, nVerbose);
     return pNew;
 }
 
@@ -1287,63 +1503,67 @@ Miaig randomReadExcept(std::vector<Miaig> &pBests, Miaig &pExcept) {
     return (pBests[iNum] == pExcept) ? pBests[(iNum + 1) % pBests.size()] : pBests[iNum];
 }
 
-Miaig Miaig::rewire(int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fCheck, Gia_ChMan_t *pChMan, int nVerbose) {
+Miaig Miaig::rewire(int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fDch, int fTiming, int fCheck, Gia_ChMan_t *pChMan, int nVerbose) {
     const int nRootSave = 8;
     const int nBestSave = 4;
+    int iter = 0;
     int nRestart = 5000;
-    std::vector<Miaig> pRoots = {this->dup(0)};
-    std::vector<Miaig> pBests = {this->dup(0)}; Miaig pInit = pBests[0];
+    std::vector<Miaig> pRoots = {this->dup(0, 0, 1)};
+    std::vector<Miaig> pBests = {this->dup(0, 0, 1)}; Miaig pInit = pBests[0];
     iword clkStart = Time_Clock();
     Miaig pNew;
     Miaig pRoot = pRoots[0];
-    Miaig pBest = this->dup(0); int improved = 0;
-    float (Miaig::*Miaig_ObjectiveFunction)(int, int) = (nMode == 0) ? &Miaig::countAnd2 : &Miaig::countTransistors;
+    Miaig pBest = this->dup(0, 0, 1); int improved = 0;
+    float (Miaig::*Miaig_ObjectiveFunction)(int, int, int) = (nMode == 0) ? (fTiming ? &Miaig::countLevel: &Miaig::countAnd2) : (fTiming ? &Miaig::countMappedDelay : &Miaig::countMappedArea);
     int maxLevel = levelGrowRatio != 0 ? this->countLevel() * levelGrowRatio : 0;
     int nExpandableLevel = maxLevel ? maxLevel - this->countLevel() : 0;
-    int fMapped = nMode > 0;
+    int fMapped = nMode == 1;
     word *pExc = _data->pExc;
 
-    float PrevBest = ((&pBest)->*Miaig_ObjectiveFunction)(1, nMappedMode);
+    float initCost = ((&pRoot)->*Miaig_ObjectiveFunction)(0, nMappedMode, fDch);
+    float bestCost = initCost;
     int iterNotImproveAfterRestart = 0;
     if (nVerbose && maxLevel) printf("Max level         : %5d\n", maxLevel);
-    if (nVerbose) printf("Initial target    : %5g (AND2 = %5g Level = %3d)\n", PrevBest, this->countAnd2(1), this->countLevel());
-    for (int i = 0; nIters ? i < nIters : 1; i++) {
-        if (nVerbose) printf("\rIteration %7d(%zu) : %5g -> ", i + 1, pBests.size(), ((&pRoot)->*Miaig_ObjectiveFunction)(0, nMappedMode));
+    if (nVerbose) printf("Initial target    : %5g (AND2 = %5g Level = %3g)\n", bestCost, this->countAnd2(1), this->countLevel());
+    for (iter = 0; nIters ? iter < nIters : 1; iter++) {
+        if (nVerbose) printf("\rIteration %7d(%zu) : %5g (AND2 = %5g Level = %3g) -> ", iter + 1, pBests.size(), ((&pRoot)->*Miaig_ObjectiveFunction)(0, nMappedMode, fDch), pRoot.countAnd2(), pRoot.countLevel());
         if (nTimeOut && nTimeOut < 1.0 * (Time_Clock() - clkStart) / CLOCKS_PER_SEC) break;
-        if (PrevBest == 0) break;
-        pNew = pRoot.dupMulti(nFaninMax, nGrowth);
+        if (bestCost == 0) break;
+        pNew = (fTiming) ? pRoot.dupExtend(nFaninMax, nGrowth) : pRoot.dupMulti(nFaninMax, nGrowth);
 
-        if (i % 2 == 0) {
-            pNew = pNew.expandThenReduce(nGrowth, nDist, nExpandableLevel, pExc, fCheck, nVerbose > 1);
+        if (iter % 2 == 0) {
+            pNew = pNew.expandThenReduce(nGrowth, nDist, nExpandableLevel, pExc, fTiming, fCheck, nVerbose > 1);
         }
-        pNew = pNew.expandShareReduce(nExpands, nDivs, nDist, nExpandableLevel, pExc, fCheck, nVerbose > 1);
+        pNew = pNew.expandShareReduce(nExpands, nDivs, nDist, nExpandableLevel, pExc, fTiming, fCheck, nVerbose > 1);
 
         ++iterNotImproveAfterRestart;
         // report
-        float rootTarget = ((&pRoot)->*Miaig_ObjectiveFunction)(0, nMappedMode);
-        float newTarget = ((&pNew)->*Miaig_ObjectiveFunction)(1, nMappedMode);
+        float rootTarget = ((&pRoot)->*Miaig_ObjectiveFunction)(0, nMappedMode, fDch);
+        float newTarget = ((&pNew)->*Miaig_ObjectiveFunction)(1, nMappedMode, fDch);
         if (maxLevel ? pNew.countLevel() > maxLevel : 0) {
-        } else if (PrevBest > newTarget) {
-            if (nVerbose) printf("%5g (AND2 = %5g Level = %3d) ", newTarget, pNew.countAnd2(), pNew.countLevel());
-            if (nVerbose) Time_PrintEndl("Elapsed time", Time_Clock() - clkStart);
-            PrevBest = newTarget;
-            pBests = {pNew.dup(0), pNew.dup(0)};
-            pBest = pNew.dup(0, fMapped), improved = 1;
-            iterNotImproveAfterRestart = 0;
-        } else if (PrevBest == newTarget) {
-            randomAddBest(pBests, pNew.dup(0), nBestSave, pChMan);
+        } else if (bestCost >= newTarget) {
+            if ((bestCost > newTarget) || (fTiming && (pNew.countAnd2() < pBest.countAnd2()))) {
+                if (nVerbose) printf("%5g (AND2 = %5g Level = %3g) ", newTarget, pNew.countAnd2(), pNew.countLevel());
+                if (nVerbose) Time_PrintEndl("Elapsed time", Time_Clock() - clkStart);
+                bestCost = newTarget;
+                pBests = {pNew.dup(0, 0, fMapped), pNew.dup(0, 0, fMapped)};
+                pBest = pNew.dup(0, 0, fMapped), improved = 1;
+                iterNotImproveAfterRestart = 0;
+            } else if (!fTiming || (fTiming && pNew.countAnd2() <= pBest.countAnd2())) {
+                randomAddBest(pBests, pNew.dup(0, 0, fMapped), nBestSave, pChMan);
+            }
         }
         // compare
         if (maxLevel ? pNew.countLevel() > maxLevel : 0) {
         } else if (rootTarget < newTarget) {
             if (iterNotImproveAfterRestart > nRestart) {
-                pNew = randomRead(pBests).dupMulti(nFaninMax, nGrowth);
-                pNew = pNew.expand(nExpands, nDist, nExpandableLevel, pExc, fCheck, nVerbose > 1);
+                pNew = (fTiming) ? randomRead(pBests).dupExtend(nFaninMax, nGrowth) : randomRead(pBests).dupMulti(nFaninMax, nGrowth);
+                pNew = pNew.expand(nExpands, nDist, nExpandableLevel, pExc, fTiming, fCheck, nVerbose > 1);
                 pNew = pNew.share(nDivs == -1 ? pNew.nObjs() : nDivs);
                 pNew = pNew.dupStrash(1, 1, 0);
                 pRoots = {pNew};
                 iterNotImproveAfterRestart = 0;
-            } else if (rootTarget * 1.05 > newTarget) {
+            } else if ((!fTiming && (rootTarget * 1.05 > newTarget))) {
                 pRoots = {pNew};
             }
         } else if (rootTarget == newTarget) {
@@ -1354,6 +1574,7 @@ Miaig Miaig::rewire(int nIters, float levelGrowRatio, int nExpands, int nGrowth,
         pRoot = randomRead(pRoots);
     }
     if (nVerbose) Time_PrintEndl("Total solving time", Time_Clock() - clkStart);
+    if (nVerbose) printf("Cumulatively reduced %s by %.2f %% (%g -> %g) after %d iterations.\n", fTiming ? "delay" : "area", 100.0*(initCost - bestCost) / (initCost), initCost, bestCost, iter);
     return improved ? pBest : randomReadExcept(pBests, pInit);
 }
 
diff --git a/src/opt/rar/rewire_miaig.h b/src/opt/rar/rewireMiaig.h
similarity index 77%
rename from src/opt/rar/rewire_miaig.h
rename to src/opt/rar/rewireMiaig.h
index ffd4043efe..8e2664653e 100644
--- a/src/opt/rar/rewire_miaig.h
+++ b/src/opt/rar/rewireMiaig.h
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [rewire_miaig.h]
+  FileName    [rewireMiaig.h]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: rewire_miaig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: rewireMiaig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -26,7 +26,7 @@
 #ifdef RW_ABC
 #include "base/abc/abc.h"
 #include "aig/miniaig/miniaig.h"
-#include "rewire_map.h"
+#include "rewireMap.h"
 #define RW_INT_MAX ABC_INT_MAX
 #define Rw_MaxInt Abc_MaxInt
 #define Rw_MinInt Abc_MinInt
@@ -57,9 +57,9 @@ static inline int Rw_LitNot( int Lit )            { assert(Lit >= 0); return Lit
 static inline int Rw_LitNotCond( int Lit, int c ) { assert(Lit >= 0); return Lit ^ (int)(c > 0);                }
 static inline int Rw_LitRegular( int Lit )        { assert(Lit >= 0); return Lit & ~01;                         }
 #endif // RW_ABC
-#include "rewire_vec.h"
-#include "rewire_tt.h"
-#include "rewire_time.h"
+#include "rewireVec.h"
+#include "rewireTt.h"
+#include "rewireTime.h"
 
 
 #include <vector>
@@ -134,7 +134,7 @@ static inline int RW_XADD(int *addr, int delta) {
 #define Miaig_CustomForEachNodeOutput(p, i)         for (i = 1 + p->nIns; i < p->nObjs; i++)
 #define Miaig_CustomForEachNodeOutputStart(p, i, s) for (i = s; i < p->nObjs; i++)
 #define Miaig_CustomForEachObj(p, i)                for (i = 0; i < p->nObjs; i++)
-#define Miaig_CustomForEachObjFanin(p, i, iLit, k)  Vi_ForEachEntry(&p->pvFans[i], iLit, k)
+#define Miaig_CustomForEachObjFanin(p, i, iLit, k)  Vi_ForEachEntry(&p->pvFanins[i], iLit, k)
 
 #define Miaig_ForEachConstInput(i)         for (i = 0; i <= _data->nIns; i++)
 #define Miaig_ForEachInput(i)              for (i = 1; i <= _data->nIns; i++)
@@ -146,8 +146,9 @@ static inline int RW_XADD(int *addr, int delta) {
 #define Miaig_ForEachNodeOutput(i)         for (i = 1 + _data->nIns; i < _data->nObjs; i++)
 #define Miaig_ForEachNodeOutputStart(i, s) for (i = s; i < _data->nObjs; i++)
 #define Miaig_ForEachObj(i)                for (i = 0; i < _data->nObjs; i++)
-#define Miaig_ForEachObjFanin(i, iLit, k)  Vi_ForEachEntry(&_data->pvFans[i], iLit, k)
-#define Miaig_ForEachObjFaninStart(i, iLit, k, s)  Vi_ForEachEntryStart(&_data->pvFans[i], iLit, k, s)
+#define Miaig_ForEachObjFanin(i, iLit, k)  Vi_ForEachEntry(&_data->pvFanins[i], iLit, k)
+#define Miaig_ForEachObjFanout(i, iVar, k)  Vi_ForEachEntry(&_data->pvFanouts[i], iVar, k)
+#define Miaig_ForEachObjFaninStart(i, iLit, k, s)  Vi_ForEachEntryStart(&_data->pvFanins[i], iLit, k, s)
 
 static inline int Rw_Lit2LitV(int *pMapV2V, int Lit) {
     assert(Lit >= 0);
@@ -171,20 +172,26 @@ struct Miaig_Data {
     int *pTravIds;         // traversal IDs
     int *pCopy;            // temp copy
     int *pRefs;            // reference counters
+    int minLevel;          // minimum level
     int *pLevel;           // levels
     int *pDist;            // distances
+    int *pRequire;         // required times
     word *pTruths[3];      // truth tables
     word *pCare;           // careset
     word *pProd;           // product
-    word *pExc;           // Exc 
+    word *pExc;            // Exc 
     vi *vOrder;            // node order
     vi *vOrderF;           // fanin order
     vi *vOrderF2;          // fanin order
     vi *vTfo;              // transitive fanout cone
-    vi *pvFans;            // the array of objects' fanins
+    vi *pvFanins;          // the array of objects' fanins (literal)
+    vi *pvFanouts;         // the array of objects' fanouts (variable)
+    vi *vCiArrs;           // the arrival times of CIs (if provided) not owned
+    vi *vCoReqs;           // the required times of COs (if provided) not owned
+    vi *vTfoArrs;          // the TFO of each
     int *pTable;           // structural hashing table
     int TableSize;         // the size of the hash table
-    float nTransistor;     // objective value
+    float objectiveValue;  // objective value
     vi *pNtkMapped;        // mapped network
 };
 
@@ -229,7 +236,9 @@ class Miaig {
     int objPiIdx(int i); // No check isPi
     int objPoIdx(int i); // No check isPo
     void print(void);
+    void printNode(int i);
     int appendObj(void);
+    void setFanin(int i, int iLit);
     void appendFanin(int i, int iLit);
     int objFaninNum(int i);
     int objFanin0(int i);
@@ -239,31 +248,39 @@ class Miaig {
     int &objTravId(int i);
     int &objCopy(int i);
     int &objDist(int i);
+    int &objRequire(int i);
     int &nTravIds(void);
     word *objTruth(int i, int n);
     vi *objFanins(int i);
+    vi *objFanouts(int i);
     int objType(int i);
     int nWords(void);
     void refObj(int iObj);
     void derefObj(int iObj);
     void derefObj_rec(int iObj, int iLitSkip);
     void setName(char *pName);
+    void setMapped(Vec_Int_t *vMapping, float objectiveValue = 0.0f);
+    void attachTiming(vi *vCiArrs, vi *vCoReqs);
+    void checkTiming(vi *vCiArrs, vi *vCoReqs);
 
 private:
     int initializeLevels_rec(int iObj);
+    void updateLevels_rec(int iObj);
     void initializeLevels(void);
     void initializeRefs(void);
     void verifyRefs(void);
     void initializeTruth(void);
     void initializeDists(void);
+    void initializeFanouts(void);
+    void initializeRequire_rec(int iObj);
+    void updateRequire_rec(int iObj);
+    void initializeRequire(void);
 
 private:
     void markDfs_rec(int iObj);
     int markDfs(void);
     void markDistanceN_rec(int iObj, int n, int limit);
     void markDistanceN(int Obj, int n);
-    void markCritical(void);
-    void markCritical_rec(int iObj);
     void topoCollect_rec(int iObj);
     vi *topoCollect(void);
     void reduceFanins(vi *v);
@@ -288,10 +305,11 @@ class Miaig {
     int *hashLookup(int *pTable, int l0, int l1, int TableSize);
 
 public:
-    float countAnd2(int reset = 0, int fDummy = 0);
+    float countAnd2(int reset = 0, int fDummy1 = 0, int fDummy2 = 0);
+    float countLevel(int reset = 0, int fDummy1 = 0, int fDummy2 = 0);
     // 0: amap 1: &nf 2: &simap
-    float countTransistors(int reset = 0, int nMode = 0);
-    int countLevel(int min = 0);
+    float countMappedArea(int reset = 0, int nMode = 0, int fDch = 1);
+    float countMappedDelay(int reset = 0, int nMode = 0, int fDch = 1);
 
 private:
     void dupDfs_rec(Miaig &pNew, int iObj);
@@ -303,21 +321,24 @@ class Miaig {
     int buildNodeCascade(Miaig &pNew, vi *vFanins, int fCprop, int fStrash);
 
 private:
-    int expandOne(int iObj, int nAddedMax, int nDist, int nExpandableLevel, word *pExc, int fCheck, int fVerbose);
-    int reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic, word *pExc, int fCheck, int fVerbose);
-    int expandThenReduceOne(int iNode, int nFaninAddLimit, int nDist, int nExpandableLevel, word *pExc, int fCheck, int fVerbose);
+    void expandOneHeuristicSort(int *pOrderF, int fTiming);
+    void reduceOneHeuristicSort(int *pOrderF, int fTiming);
+    int expandOne(int iObj, int nAddedMax, int nDist, int nExpandableLevel, word *pExc, int fTiming, int fCheck, int fVerbose);
+    int reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic, word *pExc, int fTiming, int fCheck, int fVerbose);
+    int expandThenReduceOne(int iNode, int nFaninAddLimit, int nDist, int nExpandableLevel, word *pExc, int fTiming, int fCheck, int fVerbose);
 
 public:
-    Miaig dup(int fRemDangle, int fMapped = 0);
+    Miaig dup(int fRemDangle, int fFanout, int fMapped = 0);
     Miaig dupDfs(void);
-    Miaig dupStrash(int fCprop, int fStrash, int fCascade);
-    Miaig dupMulti(int nFaninMax_, int nGrowth);
-    Miaig expand(int nFaninAddLimitAll, int nDist, int nExpandableLevel, word *pExc, int fCheck, int nVerbose);
+    Miaig dupStrash(int fCprop, int fStrash, int fCascade, int fFanout = 0);
+    Miaig dupMulti(int nFaninMax, int nGrowth);
+    Miaig dupExtend(int nFaninMax, int nGrowth);
+    Miaig expand(int nFaninAddLimitAll, int nDist, int nExpandableLevel, word *pExc, int fTiming, int fCheck, int nVerbose);
     Miaig share(int nNewNodesMax);
-    Miaig reduce(word *pExc, int fCheck, int fVerbose);
-    Miaig expandThenReduce(int nFaninAddLimit, int nDist, int nExpandableLevel, word *pExc, int fCheck, int fVerbose);
-    Miaig expandShareReduce(int nFaninAddLimitAll, int nDivs, int nDist, int nExpandableLevel, word *pExc, int fCheck, int nVerbose);
-    Miaig rewire(int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fCheck, Gia_ChMan_t *pChMan, int nVerbose);
+    Miaig reduce(word *pExc, int fTiming, int fCheck, int fVerbose);
+    Miaig expandThenReduce(int nFaninAddLimit, int nDist, int nExpandableLevel, word *pExc, int fTiming, int fCheck, int fVerbose);
+    Miaig expandShareReduce(int nFaninAddLimitAll, int nDivs, int nDist, int nExpandableLevel, word *pExc, int fTiming, int fCheck, int nVerbose);
+    Miaig rewire(int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fDch, int fTiming, int fCheck, Gia_ChMan_t *pChMan, int nVerbose);
 #ifdef RW_ABC
     Gia_Man_t *toGia(void);
     Abc_Ntk_t *toNtk(int fMapped = 0);
@@ -390,10 +411,20 @@ inline void Miaig::release(void) {
     if (_refcount && RW_XADD(_refcount, -1) == 1) {
         if (_data) {
             if (_data->pName) free(_data->pName);
-            for (int i = 0; i < _data->nObjsAlloc; ++i)
-                if (_data->pvFans[i].ptr)
-                    free(_data->pvFans[i].ptr);
-            free(_data->pvFans);
+            for (int i = 0; i < _data->nObjsAlloc; ++i) {
+                if (_data->pvFanins[i].ptr) {
+                    free(_data->pvFanins[i].ptr);
+                }
+            }
+            free(_data->pvFanins);
+            if (_data->pvFanouts) {
+                for (int i = 0; i < _data->nObjsAlloc; ++i) {
+                    if (_data->pvFanouts[i].ptr) {
+                        free(_data->pvFanouts[i].ptr);
+                    }
+                }
+                free(_data->pvFanouts);
+            }
             Vi_Free(_data->vOrder);
             Vi_Free(_data->vOrderF);
             Vi_Free(_data->vOrderF2);
@@ -407,6 +438,7 @@ inline void Miaig::release(void) {
             if (_data->pExc) free(_data->pExc);
             if (_data->pLevel) free(_data->pLevel);
             if (_data->pDist) free(_data->pDist);
+            if (_data->pRequire) free(_data->pRequire);
             if (_data->pTable) free(_data->pTable);
             if (_data->pNtkMapped) Vi_Free(_data->pNtkMapped);
             delete _data;
@@ -466,6 +498,22 @@ inline int Miaig::appendObj(void) {
 
 inline void Miaig::appendFanin(int i, int iLit) {
     Vi_PushOrder(objFanins(i), iLit);
+    if (_data->pvFanouts) {
+        Vi_PushOrder(objFanouts(Rw_Lit2Var(iLit)), i);
+    }
+}
+
+inline void Miaig::setFanin(int iObj, int iLit1) {
+    derefObj(iObj);
+    if (_data->pvFanouts) {
+        int iLit2, i;
+        Miaig_ForEachObjFanin(iObj, iLit2, i) {
+            if (Rw_Lit2Var(iLit1) == Rw_Lit2Var(iLit2)) continue;
+            Vi_Remove(objFanouts(Rw_Lit2Var(iLit2)), iObj);
+        }
+    }
+    Vi_Fill(objFanins(iObj), 1, iLit1);
+    refObj(iObj);
 }
 
 inline int Miaig::objFaninNum(int i) {
@@ -501,6 +549,10 @@ inline int &Miaig::objDist(int i) {
     return _data->pDist[i];
 }
 
+inline int &Miaig::objRequire(int i) {
+    return _data->pRequire[i];
+}
+
 inline int &Miaig::nTravIds(void) {
     return _data->nTravIds;
 }
@@ -509,7 +561,9 @@ inline int Miaig::nWords(void) {
     return _data->nWords;
 }
 
-inline float Miaig::countAnd2(int reset, int fDummy) {
+inline float Miaig::countAnd2(int reset, int fDummy1, int fDummy2) {
+    (void)fDummy1;
+    (void)fDummy2;
     int i, Counter = 0;
     Miaig_ForEachNode(i) {
         Counter += objFaninNum(i) - 1;
@@ -517,12 +571,13 @@ inline float Miaig::countAnd2(int reset, int fDummy) {
     return Counter;
 }
 
-inline int Miaig::countLevel(int min) {
+inline float Miaig::countLevel(int reset, int fDummy1, int fDummy2) {
+    (void)fDummy1;
+    (void)fDummy2;
     initializeLevels();
-    int i, Level = (min) ? RW_INT_MAX : -1;
-    int (*compareFunc)(int, int) = (min) ? Rw_MinInt : Rw_MaxInt;
+    int i, Level = -1;
     Miaig_ForEachOutput(i) {
-        Level = compareFunc(Level, objLevel(i));
+        Level = Rw_MaxInt(Level, objLevel(i));
     }
     return Level;
 }
@@ -532,13 +587,25 @@ inline word *Miaig::objTruth(int i, int n) {
 }
 
 inline vi *Miaig::objFanins(int i) {
-    return _data->pvFans + i;
+    return _data->pvFanins + i;
+}
+
+inline vi *Miaig::objFanouts(int i) {
+    assert(_data->pvFanouts);
+    return _data->pvFanouts + i;
 }
 
 inline int Miaig::objType(int i) {
     return objTravId(i) == nTravIds();
 }
 
+inline void Miaig::attachTiming(vi *vCiArrs, vi *vCoReqs) {
+    _data->vCiArrs = vCiArrs;
+    _data->vCoReqs = vCoReqs;
+    if (vCiArrs) assert(Vi_Size(vCiArrs) == nIns());
+    if (vCoReqs) assert(Vi_Size(vCoReqs) == nOuts());
+}
+
 } // namespace Rewire
 
 #ifdef RW_ABC
diff --git a/src/opt/rar/rewire_rar.c b/src/opt/rar/rewireRar.c
similarity index 73%
rename from src/opt/rar/rewire_rar.c
rename to src/opt/rar/rewireRar.c
index b0dba3381b..cd11a59da0 100644
--- a/src/opt/rar/rewire_rar.c
+++ b/src/opt/rar/rewireRar.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [rewire_rar.c]
+  FileName    [rewireRar.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,24 +14,24 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: rewire_rar.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: rewireRar.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
-#include "rewire_rar.h"
+#include "rewireRar.h"
 
 ABC_NAMESPACE_IMPL_START
 
-Gia_Man_t *Gia_ManRewire(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fChoices, int fVerbose) {
-    return Gia_ManRewireInt(pGia, pExc, nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, fCheck, fChoices, fVerbose);
+Gia_Man_t *Gia_ManRewire(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fDch, int fTiming, int nSeed, int fCheck, int fChoices, int fVerbose) {
+    return Gia_ManRewireInt(pGia, pExc, nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, fDch, fTiming, nSeed, fCheck, fChoices, fVerbose);
 }
 
-Abc_Ntk_t *Abc_ManRewire(Abc_Ntk_t *pNtk, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose) {
-    return Abc_ManRewireInt(pNtk, pExc, nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, fCheck, fVerbose);
+Abc_Ntk_t *Abc_ManRewire(Abc_Ntk_t *pNtk, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fDch, int fTiming, int nSeed, int fCheck, int fVerbose) {
+    return Abc_ManRewireInt(pNtk, pExc, nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, fDch, fTiming, nSeed, fCheck, fVerbose);
 }
 
-Mini_Aig_t *MiniAig_ManRewire(Mini_Aig_t *pAig, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose) {
-    return MiniAig_ManRewireInt(pAig, pExc, nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, fCheck, fVerbose);
+Mini_Aig_t *MiniAig_ManRewire(Mini_Aig_t *pAig, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fDch, int fTiming, int nSeed, int fCheck, int fVerbose) {
+    return MiniAig_ManRewireInt(pAig, pExc, nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, fDch, fTiming, nSeed, fCheck, fVerbose);
 }
 
 ABC_NAMESPACE_IMPL_END
\ No newline at end of file
diff --git a/src/opt/rar/rewire_rar.h b/src/opt/rar/rewireRar.h
similarity index 79%
rename from src/opt/rar/rewire_rar.h
rename to src/opt/rar/rewireRar.h
index 44f0d53424..a88f9f233a 100644
--- a/src/opt/rar/rewire_rar.h
+++ b/src/opt/rar/rewireRar.h
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [rewire_rar.h]
+  FileName    [rewireRar.h]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: rewire_rar.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: rewireRar.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -35,12 +35,12 @@
 
 ABC_NAMESPACE_HEADER_START
 
-Gia_Man_t *Gia_ManRewire(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fChoices, int fVerbose);
-Gia_Man_t *Gia_ManRewireInt(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fChoices, int fVerbose);
-Abc_Ntk_t *Abc_ManRewire(Abc_Ntk_t *pNtk, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose);
-Abc_Ntk_t *Abc_ManRewireInt(Abc_Ntk_t *pNtk, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose);
-Mini_Aig_t *MiniAig_ManRewire(Mini_Aig_t *pAig, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose);
-Mini_Aig_t *MiniAig_ManRewireInt(Mini_Aig_t *pAig, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose);
+Gia_Man_t *Gia_ManRewire(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fDch, int fTiming, int nSeed, int fCheck, int fChoices, int fVerbose);
+Gia_Man_t *Gia_ManRewireInt(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fDch, int fTiming, int nSeed, int fCheck, int fChoices, int fVerbose);
+Abc_Ntk_t *Abc_ManRewire(Abc_Ntk_t *pNtk, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fDch, int fTiming, int nSeed, int fCheck, int fVerbose);
+Abc_Ntk_t *Abc_ManRewireInt(Abc_Ntk_t *pNtk, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fDch, int fTiming, int nSeed, int fCheck, int fVerbose);
+Mini_Aig_t *MiniAig_ManRewire(Mini_Aig_t *pAig, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fDch, int fTiming, int nSeed, int fCheck, int fVerbose);
+Mini_Aig_t *MiniAig_ManRewireInt(Mini_Aig_t *pAig, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fDch, int fTiming, int nSeed, int fCheck, int fVerbose);
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/opt/rar/rewire_rng.c b/src/opt/rar/rewireRng.c
similarity index 90%
rename from src/opt/rar/rewire_rng.c
rename to src/opt/rar/rewireRng.c
index ec1bcb699f..be31ee22c5 100644
--- a/src/opt/rar/rewire_rng.c
+++ b/src/opt/rar/rewireRng.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [rewire_rng.c]
+  FileName    [rewireRng.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,11 +14,11 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: rewire_rng.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: rewireRng.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
-#include "rewire_rng.h"
+#include "rewireRng.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/opt/rar/rewire_rng.h b/src/opt/rar/rewireRng.h
similarity index 91%
rename from src/opt/rar/rewire_rng.h
rename to src/opt/rar/rewireRng.h
index c8cb1ac38f..55b6f90c8c 100644
--- a/src/opt/rar/rewire_rng.h
+++ b/src/opt/rar/rewireRng.h
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [rewire_rng.h]
+  FileName    [rewireRng.h]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: rewire_rng.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: rewireRng.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
diff --git a/src/opt/rar/rewire_time.h b/src/opt/rar/rewireTime.h
similarity index 93%
rename from src/opt/rar/rewire_time.h
rename to src/opt/rar/rewireTime.h
index 02291f492b..ac1fe0432f 100644
--- a/src/opt/rar/rewire_time.h
+++ b/src/opt/rar/rewireTime.h
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [rewire_time.h]
+  FileName    [rewireTime.h]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: rewire_time.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: rewireTime.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
diff --git a/src/opt/rar/rewire_tt.h b/src/opt/rar/rewireTt.h
similarity index 98%
rename from src/opt/rar/rewire_tt.h
rename to src/opt/rar/rewireTt.h
index ea8cc578cf..eeddc0c4eb 100644
--- a/src/opt/rar/rewire_tt.h
+++ b/src/opt/rar/rewireTt.h
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [rewire_tt.h]
+  FileName    [rewireTt.h]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: rewire_tt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: rewireTt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
diff --git a/src/opt/rar/rewire_vec.h b/src/opt/rar/rewireVec.h
similarity index 97%
rename from src/opt/rar/rewire_vec.h
rename to src/opt/rar/rewireVec.h
index 13089d01d7..6e00774a61 100644
--- a/src/opt/rar/rewire_vec.h
+++ b/src/opt/rar/rewireVec.h
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [rewire_vec.h]
+  FileName    [rewireVec.h]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: rewire_vec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: rewireVec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -30,7 +30,7 @@
 #include <assert.h>
 #include <string.h>
 
-#include "rewire_rng.h"
+#include "rewireRng.h"
 
 ABC_NAMESPACE_HEADER_START