Updates to delay optimization project.

8 files changed, 272 insertions, 30 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 6cc94574..4ec50a1f 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -2775,6 +2775,10 @@ SOURCE=.\src\opt\sbd\sbdLut.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\opt\sbd\sbdPath.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\opt\sbd\sbdSat.c
 # End Source File
 # Begin Source File
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index fccd4f63..2be65ed0 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -41010,7 +41010,7 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
     Sbd_Par_t Pars, * pPars = &Pars;
     Sbd_ParSetDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KSNPWFMCacvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KSNPWFMCmcdpvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -41102,11 +41102,17 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nBTLimit < 0 )
                 goto usage;
             break;
-        case 'a':
-            pPars->fArea ^= 1;
+        case 'm':
+            pPars->fMapping ^= 1;
             break;
         case 'c':
-            pPars->fCover ^= 1;
+            pPars->fMoreCuts ^= 1;
+            break;
+        case 'd':
+            pPars->fFindDivs ^= 1;
+            break;
+        case 'p':
+            pPars->fUsePath ^= 1;
             break;
         case 'v':
             pPars->fVerbose ^= 1;
@@ -41122,25 +41128,22 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9Mfs(): There is no AIG.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9Mfsd(): There is no AIG.\n" );
         return 0;
     }
     if ( Gia_ManBufNum(pAbc->pGia) )
     {
-        Abc_Print( -1, "Abc_CommandAbc9Mfs(): This command does not work with barrier buffers.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9Mfsd(): This command does not work with barrier buffers.\n" );
         return 1;
     }
     if ( Gia_ManHasMapping(pAbc->pGia) )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current AIG has mapping (run &st to unmap).\n" );
-        return 0;
-    }
+        Abc_Print( 1, "The current AIG has mapping, which can be used to determine critical path if \"-p\" is selected.\n" );
     pTemp = Sbd_NtkPerform( pAbc->pGia, pPars );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &mfsd [-KSNPWFMC <num>] [-acvwh]\n" );
+    Abc_Print( -2, "usage: &mfsd [-KSNPWFMC <num>] [-mcdpvwh]\n" );
     Abc_Print( -2, "\t           performs SAT-based delay-oriented AIG optimization\n" );
     Abc_Print( -2, "\t-K <num> : the LUT size for delay minimization (2 <= num <= 6) [default = %d]\n",         pPars->nLutSize );
     Abc_Print( -2, "\t-S <num> : the LUT structure size (1 <= num <= 2) [default = %d]\n",                      pPars->nLutNum );
@@ -41150,8 +41153,10 @@ usage:
     Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n",                pPars->nTfoFanMax );
     Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n",    pPars->nWinSizeMax );
     Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n",   pPars->nBTLimit );
-    Abc_Print( -2, "\t-a       : toggle minimizing area or area+edges [default = %s]\n",                        pPars->fArea? "area": "area+edges" );
-    Abc_Print( -2, "\t-c       : toggle using complete slow covering procedure [default = %s]\n",               pPars->fCover? "yes": "no" );
+    Abc_Print( -2, "\t-m       : toggle generating delay-oriented mapping [default = %s]\n",                    pPars->fMapping? "area": "area+edges" );
+    Abc_Print( -2, "\t-c       : toggle using several cuts at each node [default = %s]\n",                      pPars->fMoreCuts? "yes": "no" );
+    Abc_Print( -2, "\t-d       : toggle additional search for good divisors [default = %s]\n",                  pPars->fFindDivs? "yes": "no" );
+    Abc_Print( -2, "\t-p       : toggle optimizing critical path only [default = %s]\n",                        pPars->fUsePath? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n",                        pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w       : toggle printing detailed stats for each node [default = %s]\n",                pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");
diff --git a/src/opt/sbd/module.make b/src/opt/sbd/module.make
index a9a6c3be..fc176715 100644
--- a/src/opt/sbd/module.make
+++ b/src/opt/sbd/module.make
@@ -4,5 +4,6 @@ SRC +=    src/opt/sbd/sbd.c \
     src/opt/sbd/sbdCut.c \
     src/opt/sbd/sbdCut2.c \
     src/opt/sbd/sbdLut.c \
+    src/opt/sbd/sbdPath.c \
     src/opt/sbd/sbdSat.c \
     src/opt/sbd/sbdWin.c
diff --git a/src/opt/sbd/sbd.h b/src/opt/sbd/sbd.h
index 6e0f6b3b..9c419b16 100644
--- a/src/opt/sbd/sbd.h
+++ b/src/opt/sbd/sbd.h
@@ -47,6 +47,10 @@ struct Sbd_Par_t_
     int             nWinSizeMax;  // maximum window size (windowing)
     int             nBTLimit;     // maximum number of SAT conflicts 
     int             nWords;       // simulation word count
+    int             fMapping;     // generate mapping
+    int             fMoreCuts;    // use several cuts
+    int             fFindDivs;    // perform divisor search
+    int             fUsePath;     // optimize only critical path
     int             fArea;        // area-oriented optimization
     int             fCover;       // use complete cover procedure
     int             fVerbose;     // verbose flag
diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c
index 988ad3db..275d866f 100644
--- a/src/opt/sbd/sbdCore.c
+++ b/src/opt/sbd/sbdCore.c
@@ -38,6 +38,7 @@ struct Sbd_Man_t_
     Vec_Wec_t *     vTfos;       // TFO for each node (roots are marked) (windowing)
     Vec_Int_t *     vLutLevs;    // LUT level for each node after resynthesis
     Vec_Int_t *     vLutCuts;    // LUT cut for each nodes after resynthesis
+    Vec_Int_t *     vLutCuts2;   // LUT cut for each nodes after resynthesis
     Vec_Int_t *     vMirrors;    // alternative node
     Vec_Wrd_t *     vSims[4];    // simulation information (main, backup, controlability)
     Vec_Int_t *     vCover;      // temporary
@@ -73,7 +74,8 @@ struct Sbd_Man_t_
     sat_solver *    pSat;        // SAT solver
 };
 
-static inline int *  Sbd_ObjCut( Sbd_Man_t * p, int i )  { return Vec_IntEntryP( p->vLutCuts, (p->pPars->nLutSize + 1) * i ); }
+static inline int *  Sbd_ObjCut( Sbd_Man_t * p, int i )  { return Vec_IntEntryP( p->vLutCuts,  (p->pPars->nLutSize + 1) * i ); }
+static inline int *  Sbd_ObjCut2( Sbd_Man_t * p, int i ) { return Vec_IntEntryP( p->vLutCuts2, (p->pPars->nLutSize + 1) * i ); }
 
 static inline word * Sbd_ObjSim0( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[0], p->pPars->nWords * i );         }
 static inline word * Sbd_ObjSim1( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[1], p->pPars->nWords * i );         }
@@ -107,6 +109,10 @@ void Sbd_ParSetDefault( Sbd_Par_t * pPars )
     pPars->nWinSizeMax  = 2000; // maximum window size (windowing)
     pPars->nBTLimit     = 0;    // maximum number of SAT conflicts 
     pPars->nWords       = 1;    // simulation word count
+    pPars->fMapping     = 1;    // generate mapping
+    pPars->fMoreCuts    = 0;    // use several cuts
+    pPars->fFindDivs    = 0;    // perform divisor search
+    pPars->fUsePath     = 0;    // optimize only critical path
     pPars->fArea        = 0;    // area-oriented optimization
     pPars->fCover       = 0;    // use complete cover procedure
     pPars->fVerbose     = 0;    // verbose flag
@@ -231,8 +237,13 @@ Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars )
         for ( w = 0; w < p->pPars->nWords; w++ )
             Sbd_ObjSim0(p, Id)[w] = Gia_ManRandomW( 0 );     
     // cut enumeration
-    p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, pPars->nLutSize, pPars->nCutNum, 1, 1 );
-    p->pSrv = Sbd_ManCutServerStart( pGia, p->vMirrors, p->vLutLevs, NULL, NULL, pPars->nLutSize, pPars->nCutSize, pPars->nCutNum, 0 );
+    if ( pPars->fMoreCuts )
+        p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, pPars->nCutSize, pPars->nCutNum, !pPars->fMapping, 1 );
+    else
+    {
+        p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, pPars->nLutSize, pPars->nCutNum, !pPars->fMapping, 1 );
+        p->pSrv = Sbd_ManCutServerStart( pGia, p->vMirrors, p->vLutLevs, NULL, NULL, pPars->nLutSize, pPars->nCutSize, pPars->nCutNum, 0 );
+    }
     return p;
 }
 void Sbd_ManStop( Sbd_Man_t * p )
@@ -258,8 +269,8 @@ void Sbd_ManStop( Sbd_Man_t * p )
     Vec_IntFree( p->vCounts[1] );
     Vec_WrdFree( p->vMatrix );
     sat_solver_delete_p( &p->pSat );
-    Sbd_StoFree( p->pSto );
-    Sbd_ManCutServerStop( p->pSrv );
+    if ( p->pSto ) Sbd_StoFree( p->pSto );
+    if ( p->pSrv ) Sbd_ManCutServerStop( p->pSrv );
     ABC_FREE( p );
 }
 
@@ -1830,7 +1841,7 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
 
 int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
 {
-    Gia_Obj_t * pObj = NULL;
+    //Gia_Obj_t * pObj = NULL;
     int i, k, w, iLit, Node;
     int iObjLast = Gia_ManObjNum(p->pGia);
     int iCurLev = Vec_IntEntry(p->vLutLevs, Pivot);
@@ -1903,6 +1914,7 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
         //Vec_IntPush( p->vLevs, 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, Gia_ObjFaninId0(pObjI, i)), Vec_IntEntry(p->vLevs, Gia_ObjFaninId1(pObjI, i))) );
         Vec_IntPush( p->vObj2Var, 0 );
         Vec_IntFillExtra( p->vLutCuts, Vec_IntSize(p->vLutCuts) + p->pPars->nLutSize + 1, 0 );
+        Sbd_StoSaveBestDelayCut( p->pSto, i, Sbd_ObjCut(p, i) );
         //Sbd_ManFindCut( p, i, p->vLits );
         for ( k = 0; k < 4; k++ )
             for ( w = 0; w < p->pPars->nWords; w++ )
@@ -1912,7 +1924,7 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
     iNewLev = Vec_IntEntry( p->vLutLevs, Abc_Lit2Var(iLit) );
     assert( !iNewLev || iNewLev < iCurLev );
     // update delay of the initial node
-    pObj = Gia_ManObj( p->pGia, Pivot );
+    //pObj = Gia_ManObj( p->pGia, Pivot );
     assert( Vec_IntEntry(p->vLutLevs, Pivot) == iCurLev );
     Vec_IntWriteEntry( p->vLutLevs, Pivot, iNewLev );
     //Vec_IntWriteEntry( p->vLevs, Pivot, Pivot ? 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, Gia_ObjFaninId0(pObj, Pivot)), Vec_IntEntry(p->vLevs, Gia_ObjFaninId1(pObj, Pivot))) : 0 );
@@ -1930,6 +1942,70 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
   SeeAlso     []
 
 ***********************************************************************/
+void Sbd_ManDeriveMapping_rec( Sbd_Man_t * p, Gia_Man_t * pNew, int iObj )
+{
+    Gia_Obj_t * pObj; int k, * pCut;
+    if ( Gia_ObjIsTravIdCurrentId(pNew, iObj) )
+        return;
+    Gia_ObjSetTravIdCurrentId(pNew, iObj);
+    pObj = Gia_ManObj( pNew, iObj );
+    if ( Gia_ObjIsCi(pObj) )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    pCut = Sbd_ObjCut2( p, iObj );
+    for ( k = 1; k <= pCut[0]; k++ )
+        Sbd_ManDeriveMapping_rec( p, pNew, pCut[k] );
+    // add mapping
+    Vec_IntWriteEntry( pNew->vMapping, iObj, Vec_IntSize(pNew->vMapping) );
+    for ( k = 0; k <= pCut[0]; k++ )
+        Vec_IntPush( pNew->vMapping, pCut[k] );
+    Vec_IntPush( pNew->vMapping, iObj );
+}
+void Sbd_ManDeriveMapping( Sbd_Man_t * p, Gia_Man_t * pNew )
+{
+    Gia_Obj_t * pObj, * pFan; 
+    int i, k, iFan, iObjNew, * pCut, * pCutNew;
+    Vec_Int_t * vLeaves = Vec_IntAlloc( 100 );
+    // derive cuts for the new manager
+    p->vLutCuts2 = Vec_IntStart( Gia_ManObjNum(pNew) * (p->pPars->nLutSize + 1) );
+    Gia_ManForEachAnd( p->pGia, pObj, i )
+    {
+        if ( Vec_IntEntry(p->vMirrors, i) >= 0 )
+            continue;
+        if ( pObj->Value == ~0 )
+            continue;
+        iObjNew = Abc_Lit2Var( pObj->Value );
+        if ( !Gia_ObjIsAnd(Gia_ManObj(pNew, iObjNew)) )
+            continue;
+        pCutNew = Sbd_ObjCut2( p, iObjNew );
+        pCut    = Sbd_ObjCut( p, i );
+        Vec_IntClear( vLeaves );
+        for ( k = 1; k <= pCut[0]; k++ )
+        {
+            iFan = Vec_IntEntry(p->vMirrors, pCut[k]) >= 0 ? Abc_Lit2Var(Vec_IntEntry(p->vMirrors, pCut[k])) : pCut[k];
+            pFan = Gia_ManObj( p->pGia, iFan );
+            if ( pFan->Value == ~0 )
+                continue;
+            iObjNew = Abc_Lit2Var( pFan->Value );
+            if ( iObjNew == 0 )
+                continue;
+            Vec_IntPushUniqueOrder( vLeaves, iObjNew );
+        }
+        assert( Vec_IntSize(vLeaves) <= p->pPars->nLutSize );
+        assert( Vec_IntSize(vLeaves) > 1 );
+        pCutNew[0] = Vec_IntSize(vLeaves);
+        memcpy( pCutNew+1, Vec_IntArray(vLeaves), sizeof(int) * Vec_IntSize(vLeaves) );
+    }
+    Vec_IntFree( vLeaves );
+    // create new mapping
+    Vec_IntFreeP( &pNew->vMapping );
+    pNew->vMapping = Vec_IntAlloc( (p->pPars->nLutSize + 2) * Gia_ManObjNum(pNew) );
+    Vec_IntFill( pNew->vMapping, Gia_ManObjNum(pNew), 0 );
+    Gia_ManIncrementTravId( pNew );
+    Gia_ManForEachCo( pNew, pObj, i )
+        Sbd_ManDeriveMapping_rec( p, pNew, Gia_ObjFaninId0p(pNew, pObj) );
+    Vec_IntFreeP( &p->vLutCuts2 );
+}
 void Sbd_ManDerive_rec( Gia_Man_t * pNew, Gia_Man_t * p, int Node, Vec_Int_t * vMirrors )
 {
     Gia_Obj_t * pObj;
@@ -1951,7 +2027,7 @@ void Sbd_ManDerive_rec( Gia_Man_t * pNew, Gia_Man_t * p, int Node, Vec_Int_t * v
     if ( Obj != Node )
         Gia_ManObj(p, Node)->Value = Abc_LitNotCond( pObj->Value, Abc_LitIsCompl(Vec_IntEntry(vMirrors, Node)) );
 } 
-Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
+Gia_Man_t * Sbd_ManDerive( Sbd_Man_t * pMan, Gia_Man_t * p, Vec_Int_t * vMirrors )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
@@ -1973,9 +2049,12 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
     Gia_ManHashStop( pNew );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     Gia_ManTransferTiming( pNew, p );
+    if ( pMan->pPars->fMapping )
+        Sbd_ManDeriveMapping( pMan, pNew );
     // remove dangling nodes
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManTransferTiming( pNew, pTemp );
+    Gia_ManTransferMapping( pNew, pTemp );
     Gia_ManStop( pTemp );
     return pNew;
 }
@@ -1993,7 +2072,7 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
 ***********************************************************************/
 void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
 {
-    Sbd_Str_t Strs[SBD_DIV_MAX]; //word Truth = 0;
+    Sbd_Str_t Strs[SBD_DIV_MAX]; word Truth = 0;
     int RetValue, nStrs = 0;
     if ( !p->pSto && Sbd_ManMergeCuts( p, Pivot ) )
         return;
@@ -2009,8 +2088,7 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
         Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue );
         if ( p->pPars->fVerbose ) printf( "Node %5d:  Detected constant %d.\n", Pivot, RetValue );
     }
-/*
-    else if ( p->pPars->nLutNum >= 1 && Sbd_ManExplore2( p, Pivot, &Truth ) )
+    else if ( p->pPars->fFindDivs && p->pPars->nLutNum >= 1 && Sbd_ManExplore2( p, Pivot, &Truth ) )
     {
         int i;
         Strs->fLut = 1;
@@ -2021,7 +2099,6 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
         Sbd_ManImplement2( p, Pivot, 1, Strs );
         if ( p->pPars->fVerbose ) printf( "Node %5d:  Detected LUT%d\n", Pivot, p->pPars->nLutSize );
     }
-*/
     else if ( p->pPars->nLutNum >= 2 && Sbd_ManExplore3( p, Pivot, &nStrs, Strs ) )
     {
         Sbd_ManImplement2( p, Pivot, nStrs, Strs );
@@ -2041,6 +2118,7 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
 {
     Gia_Man_t * pNew;  
     Gia_Obj_t * pObj;
+    Vec_Bit_t * vPath;
     Sbd_Man_t * p = Sbd_ManStart( pGia, pPars );
     int nNodesOld = Gia_ManObjNum(pGia);
     int k, Pivot;
@@ -2049,6 +2127,7 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
     Gia_ManForEachObj( p->pGia, pObj, Pivot )
         Sbd_StoRefObj( p->pSto, Pivot, -1 );
     //return NULL;
+    vPath = (pPars->fUsePath && Gia_ManHasMapping(pGia)) ? Sbc_ManCriticalPath(pGia) : NULL;
     if ( pGia->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)pGia->pManTime) )
     {
         Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( pGia );
@@ -2065,9 +2144,10 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
             {
                 abctime clk = Abc_Clock();
                 int Delay = Sbd_StoComputeCutsNode( p->pSto, Pivot );
+                Sbd_StoSaveBestDelayCut( p->pSto, Pivot, Sbd_ObjCut(p, Pivot) );
                 p->timeCut += Abc_Clock() - clk;
                 Vec_IntWriteEntry( p->vLutLevs, Pivot, Delay );
-                if ( Delay > 1 )//&& Gia_ObjRefNumId(p->pGia, Pivot) > 1 )
+                if ( Delay > 1 && (!vPath || Vec_BitEntry(vPath, Pivot)) )
                     Sbd_NtkPerformOne( p, Pivot );
             }
             else if ( Gia_ObjIsCi(pObj) )
@@ -2102,22 +2182,25 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
             {
                 abctime clk = Abc_Clock();
                 int Delay = Sbd_StoComputeCutsNode( p->pSto, Pivot );
+                Sbd_StoSaveBestDelayCut( p->pSto, Pivot, Sbd_ObjCut(p, Pivot) );
                 p->timeCut += Abc_Clock() - clk;
                 Vec_IntWriteEntry( p->vLutLevs, Pivot, Delay );
-                if ( Delay > 1 )//&& Gia_ObjRefNumId(p->pGia, Pivot) > 1 )
+                if ( Delay > 1 && (!vPath || Vec_BitEntry(vPath, Pivot)) )
                     Sbd_NtkPerformOne( p, Pivot );
             }
             //if ( nNodesOld != Gia_ManObjNum(pGia) )
             //    break;
         }
     }
+    Vec_BitFreeP( &vPath );
     printf( "K = %d. S = %d. N = %d. P = %d.  ", 
         p->pPars->nLutSize, p->pPars->nLutNum, p->pPars->nCutSize, p->pPars->nCutNum );
     printf( "Try = %d. Use = %d.  C = %d. 1 = %d. 2 = %d. 3a = %d. 3b = %d.  Lev = %d.  ", 
         p->nTried, p->nUsed, p->nLuts[0], p->nLuts[1], p->nLuts[2], p->nLuts[3], p->nLuts[4], Sbd_ManDelay(p) );
     p->timeTotal = Abc_Clock() - p->timeTotal;
     Abc_PrintTime( 1, "Time", p->timeTotal );
-    pNew = Sbd_ManDerive( pGia, p->vMirrors );
+    //Sbd_ManDeriveMapping2( p );
+    pNew = Sbd_ManDerive( p, pGia, p->vMirrors );
     // print runtime statistics
     p->timeOther = p->timeTotal - p->timeWin - p->timeCut - p->timeCov - p->timeCnf - p->timeSat - p->timeQbf;
     //if ( p->pPars->fVerbose )
diff --git a/src/opt/sbd/sbdCut.c b/src/opt/sbd/sbdCut.c
index 7bcf2189..59505c98 100644
--- a/src/opt/sbd/sbdCut.c
+++ b/src/opt/sbd/sbdCut.c
@@ -65,10 +65,11 @@ struct Sbd_Sto_t_
     Sbd_Cut_t *     ppCuts[SBD_MAX_CUTNUM];    // temporary cut pointers
     int             nCutsR;                    // the number of cuts
     int             Pivot;                     // current object
-    double          CutCount[4];               // cut counters
+    int             iCutBest;                  // best-delay cut
     int             nCutsSpec;                 // special cuts
     int             nCutsOver;                 // overflow cuts
     int             DelayMin;                  // minimum delay
+    double          CutCount[4];               // cut counters
     abctime         clkStart;                  // starting time
 };
 
@@ -540,6 +541,7 @@ static inline void Sbd_StoComputeDelay( Sbd_Sto_t * p, int iObj, Sbd_Cut_t ** pC
 {
     int i, v, Delay, DelayMin = ABC_INFINITY;
     assert( nCuts > 0 );
+    p->iCutBest = -1;
     for ( i = 0; i < nCuts; i++ )
     {
         if ( (int)pCuts[i]->nLeaves > p->nLutSize )
@@ -547,8 +549,16 @@ static inline void Sbd_StoComputeDelay( Sbd_Sto_t * p, int iObj, Sbd_Cut_t ** pC
         Delay = 0;
         for ( v = 0; v < (int)pCuts[i]->nLeaves; v++ )
             Delay = Abc_MaxInt( Delay, Vec_IntEntry(p->vDelays, pCuts[i]->pLeaves[v]) );
-        DelayMin = Abc_MinInt( DelayMin, Delay );
+        //DelayMin = Abc_MinInt( DelayMin, Delay );
+        if ( DelayMin > Delay )
+        {
+            DelayMin = Delay;
+            p->iCutBest = i;
+        }
+        else if ( DelayMin == Delay && p->iCutBest >= 0 && pCuts[p->iCutBest]->nLeaves > pCuts[i]->nLeaves )
+            p->iCutBest = i;
     }
+    assert( p->iCutBest >= 0 );
     assert( DelayMin < ABC_INFINITY );
     DelayMin = (nCuts > 1 || pCuts[0]->nLeaves > 1) ? DelayMin + 1 : DelayMin;
     Vec_IntWriteEntry( p->vDelays, iObj, DelayMin );
@@ -725,6 +735,14 @@ int Sbd_StoComputeCutsNode( Sbd_Sto_t * p, int iObj )
     Sbd_StoMergeCuts( p, iObj );
     return Vec_IntEntry( p->vDelays, iObj );
 }
+void Sbd_StoSaveBestDelayCut( Sbd_Sto_t * p, int iObj, int * pCut )
+{
+    Sbd_Cut_t * pCutBest = p->ppCuts[p->iCutBest]; int i;
+    assert( iObj == p->Pivot );
+    pCut[0] = pCutBest->nLeaves;
+    for ( i = 0; i < (int)pCutBest->nLeaves; i++ )
+        pCut[i+1] = pCutBest->pLeaves[i];
+}
 int Sbd_StoObjRefs( Sbd_Sto_t * p, int iObj )
 {
     return Vec_IntEntry(p->vRefs, iObj);
diff --git a/src/opt/sbd/sbdInt.h b/src/opt/sbd/sbdInt.h
index 9b489854..eabe5355 100644
--- a/src/opt/sbd/sbdInt.h
+++ b/src/opt/sbd/sbdInt.h
@@ -92,6 +92,7 @@ extern void         Sbd_StoComputeCutsConst0( Sbd_Sto_t * p, int iObj );
 extern void         Sbd_StoComputeCutsObj( Sbd_Sto_t * p, int iObj, int Delay, int Level );
 extern void         Sbd_StoComputeCutsCi( Sbd_Sto_t * p, int iObj, int Delay, int Level );
 extern int          Sbd_StoComputeCutsNode( Sbd_Sto_t * p, int iObj );
+extern void         Sbd_StoSaveBestDelayCut( Sbd_Sto_t * p, int iObj, int * pCut );
 extern int          Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int nSize, int * pLeaves );
 /*=== sbdCut2.c ==========================================================*/
 extern Sbd_Srv_t *  Sbd_ManCutServerStart( Gia_Man_t * pGia, Vec_Int_t * vMirrors, 
@@ -104,6 +105,8 @@ extern word         Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar,
 extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
 extern int          Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds );
 extern int          Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset );
+/*=== sbdPath.c ==========================================================*/
+extern Vec_Bit_t *  Sbc_ManCriticalPath( Gia_Man_t * p );
 /*=== sbdQbf.c ==========================================================*/
 extern int          Sbd_ProblemSolve( 
                                        Gia_Man_t * p, Vec_Int_t * vMirrors, 
diff --git a/src/opt/sbd/sbdPath.c b/src/opt/sbd/sbdPath.c
new file mode 100644
index 00000000..417cb407
--- /dev/null
+++ b/src/opt/sbd/sbdPath.c
@@ -0,0 +1,124 @@
+/**CFile****************************************************************
+
+  FileName    [sbdPath.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    [Critical path.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sbdPath.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sbc_ManAddInternalToPath_rec( Gia_Man_t * p, int iObj, Vec_Bit_t * vPath )
+{
+    Gia_Obj_t * pObj; 
+    int k, iFan, Value = 0;
+    if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
+        return Vec_BitEntry(vPath, iObj);
+    Gia_ObjSetTravIdCurrentId(p, iObj);
+    pObj = Gia_ManObj( p, iObj );
+    if ( Gia_ObjIsCi(pObj) )
+        return 0;
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_LutForEachFanin( p, iObj, iFan, k )
+        Value |= Sbc_ManAddInternalToPath_rec( p, iFan, vPath );
+    if ( Value )
+        Vec_BitWriteEntry( vPath, iObj, 1 );
+    return Value;
+}
+void Sbc_ManAddInternalToPath( Gia_Man_t * p, Vec_Bit_t * vPath )
+{
+    int iObj;
+    Gia_ManForEachLut( p, iObj )
+    {
+        if ( !Vec_BitEntry(vPath, iObj) )
+            continue;
+        Gia_ManIncrementTravId( p );
+        Sbc_ManAddInternalToPath_rec( p, iObj, vPath );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sbc_ManCriticalPath_rec( Gia_Man_t * p, int * pLevels, int iObj, int LevelFan, Vec_Bit_t * vPath )
+{
+    Gia_Obj_t * pObj; int k, iFan;
+    if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
+        return;
+    Gia_ObjSetTravIdCurrentId(p, iObj);
+    pObj = Gia_ManObj( p, iObj );
+    if ( Gia_ObjIsCi(pObj) )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Vec_BitWriteEntry( vPath, iObj, 1 );
+    Gia_LutForEachFanin( p, iObj, iFan, k )
+        if ( pLevels[iFan] == LevelFan )
+            Sbc_ManCriticalPath_rec( p, pLevels, iFan, LevelFan-1, vPath );
+}
+Vec_Bit_t * Sbc_ManCriticalPath( Gia_Man_t * p )
+{
+    int * pLevels = NULL, k, iDriver;
+    int nLevels = p->pManTime ? Gia_ManLutLevelWithBoxes(p) : Gia_ManLutLevel(p, &pLevels);
+    Vec_Bit_t * vPath = Vec_BitStart( Gia_ManObjNum(p) );
+    if ( p->pManTime )
+        pLevels = Vec_IntArray( p->vLevels );
+    Gia_ManIncrementTravId( p );
+    Gia_ManForEachCoDriverId( p, iDriver, k )
+        if ( pLevels[iDriver] == nLevels && iDriver )
+            Sbc_ManCriticalPath_rec( p, pLevels, iDriver, nLevels-1, vPath );
+    if ( !p->pManTime )
+        ABC_FREE( pLevels );
+    Sbc_ManAddInternalToPath( p, vPath );
+    return vPath;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+