Version abc80430

24 files changed, 2084 insertions, 68 deletions

diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 41a62484..47ee8d4d 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -350,10 +350,10 @@ void Aig_ManPrintStats( Aig_Man_t * p )
 ***********************************************************************/
 void Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew )
 {
-    printf( "REGs: Beg = %d. End = %d. (R = %6.2f %%).  ",
+    printf( "REG: Beg = %5d. End = %5d. (R =%5.1f %%)  ",
         Aig_ManRegNum(p), Aig_ManRegNum(pNew), 
         Aig_ManRegNum(p)? 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pNew))/Aig_ManRegNum(p) : 0.0 );
-    printf( "ANDs: Beg = %d. End = %d. (R = %6.2f %%).",
+    printf( "AND: Beg = %6d. End = %6d. (R =%5.1f %%)",
         Aig_ManNodeNum(p), Aig_ManNodeNum(pNew), 
         Aig_ManNodeNum(p)? 100.0*(Aig_ManNodeNum(p)-Aig_ManNodeNum(pNew))/Aig_ManNodeNum(p) : 0.0 );
     printf( "\n" );
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index 00a8159e..c2d08350 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -451,27 +451,17 @@ Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose )
     Aig_Man_t * pTemp;
     Vec_Ptr_t * vMap;
     int nSaved, nCur;
+    if ( fVerbose )
+        printf( "Performing combinational register sweep:\n" );
     for ( nSaved = 0; (nCur = Aig_ManReduceLachesCount(p)); nSaved += nCur )
     {
-        if ( fVerbose )
-        {
-        printf( "Saved = %5d.   ", nCur );
-        printf( "RBeg = %5d. NBeg = %6d.   ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
-        }
         vMap = Aig_ManReduceLachesOnce( p );
-//Aig_ManPrintStats( p );
         p = Aig_ManRemap( pTemp = p, vMap );
-//Aig_ManPrintStats( p );
-        Aig_ManStop( pTemp );
         Vec_PtrFree( vMap );
         Aig_ManSeqCleanup( p );
-//Aig_ManPrintStats( p );
-//printf( "\n" );
         if ( fVerbose )
-        {
-        printf( "REnd = %5d. NEnd = %6d.   ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
-        printf( "\n" );
-        }
+            Aig_ManReportImprovement( pTemp, p );
+        Aig_ManStop( pTemp );
         if ( p->nRegs == 0 )
             break;
     }
@@ -600,6 +590,8 @@ void Aig_ManComputeSccs( Aig_Man_t * p )
 ***********************************************************************/
 Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose )
 {
+    extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
+
     Aig_Man_t * pAigInit, * pAigNew;
     Aig_Obj_t * pFlop1, * pFlop2;
     int i, Entry1, Entry2, nTruePis;
@@ -633,6 +625,8 @@ Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int
 //    Aig_ManSeqCleanup( pAigInit );
     pAigNew = Aig_ManDupRepr( pAigInit, 0 );
     Aig_ManSeqCleanup( pAigNew );
+
+    Saig_ManReportUselessRegisters( pAigNew );
     return pAigNew;
 }
 
diff --git a/src/aig/aig/aigTsim.c b/src/aig/aig/aigTsim.c
index 1d974778..d3f78902 100644
--- a/src/aig/aig/aigTsim.c
+++ b/src/aig/aig/aigTsim.c
@@ -479,14 +479,12 @@ Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose )
     Vec_Ptr_t * vMap;
     while ( (vMap = Aig_ManTernarySimulate( p, fVerbose )) )
     {
-        if ( fVerbose )
-        printf( "RBeg = %5d. NBeg = %6d.   ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
         p = Aig_ManRemap( pTemp = p, vMap );
-        Aig_ManStop( pTemp );
         Vec_PtrFree( vMap );
         Aig_ManSeqCleanup( p );
         if ( fVerbose )
-        printf( "REnd = %5d. NEnd = %6d.  \n", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
+            Aig_ManReportImprovement( pTemp, p );
+        Aig_ManStop( pTemp );
     }
     return p;
 }
diff --git a/src/aig/mfx/mfxCore.c b/src/aig/mfx/mfxCore.c
index 8867f7c1..48107e7e 100644
--- a/src/aig/mfx/mfxCore.c
+++ b/src/aig/mfx/mfxCore.c
@@ -245,7 +245,7 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib )
     p->nFaninMax = nFaninMax;
     if ( !pPars->fResub )
     {
-        pDecPars->nVarsMax = nFaninMax;
+        pDecPars->nVarsMax = (nFaninMax < 3) ? 3 : nFaninMax;
         pDecPars->fVerbose = pPars->fVerbose;
         p->vTruth = Vec_IntAlloc( 0 );
         p->pManDec = Bdc_ManAlloc( pDecPars );
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index 3902ce70..7de3ccdc 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -1,3 +1,5 @@
 SRC +=    src/aig/saig/saig_.c \
     src/aig/saig/saigPhase.c \
-    src/aig/saig/saigRetMin.c
+    src/aig/saig/saigRetFwd.c \
+    src/aig/saig/saigRetMin.c \
+    src/aig/saig/saigScl.c
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index ce09fd32..e399b8bb 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -49,6 +49,11 @@ static inline int          Saig_ManRegNum( Aig_Man_t * p )         { return p->n
 static inline Aig_Obj_t *  Saig_ManLo( Aig_Man_t * p, int i )      { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Saig_ManPiNum(p)+i);   }
 static inline Aig_Obj_t *  Saig_ManLi( Aig_Man_t * p, int i )      { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Saig_ManPoNum(p)+i);   }
 
+static inline int          Saig_ObjIsPi( Aig_Man_t * p, Aig_Obj_t * pObj )    { return Aig_ObjIsPi(pObj) && Aig_ObjPioNum(pObj) < Saig_ManPiNum(p); }
+static inline int          Saig_ObjIsPo( Aig_Man_t * p, Aig_Obj_t * pObj )    { return Aig_ObjIsPo(pObj) && Aig_ObjPioNum(pObj) < Saig_ManPoNum(p); }
+static inline int          Saig_ObjIsLo( Aig_Man_t * p, Aig_Obj_t * pObj )    { return Aig_ObjIsPi(pObj) && Aig_ObjPioNum(pObj) >= Saig_ManPiNum(p); }
+static inline int          Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj )    { return Aig_ObjIsPo(pObj) && Aig_ObjPioNum(pObj) >= Saig_ManPoNum(p); }
+
 // iterator over the primary inputs/outputs
 #define Saig_ManForEachPi( p, pObj, i )                                           \
     Vec_PtrForEachEntryStop( p->vPis, pObj, i, Saig_ManPiNum(p) )
@@ -69,7 +74,15 @@ static inline Aig_Obj_t *  Saig_ManLi( Aig_Man_t * p, int i )      { return (Aig
 ////////////////////////////////////////////////////////////////////////
 
 /*=== saigPhase.c ==========================================================*/
- 
+extern Aig_Man_t *       Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose );
+/*=== saigRetFwd.c ==========================================================*/
+extern Aig_Man_t *       Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose );
+/*=== saigRetMin.c ==========================================================*/
+extern Aig_Man_t *       Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut );
+extern Aig_Man_t *       Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
+/*=== saigScl.c ==========================================================*/
+extern void              Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
+
 #ifdef __cplusplus
 }
 #endif
diff --git a/src/aig/saig/saigRetFwd.c b/src/aig/saig/saigRetFwd.c
new file mode 100644
index 00000000..b6321da6
--- /dev/null
+++ b/src/aig/saig/saigRetFwd.c
@@ -0,0 +1,242 @@
+/**CFile****************************************************************
+
+  FileName    [saigRetFwd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Most-forward retiming.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigRetFwd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Aig_Obj_t * Aig_ObjFanoutStatic( Aig_Obj_t * pObj, int i )               { return ((Aig_Obj_t **)pObj->pData)[i];             }
+static inline void        Aig_ObjSetFanoutStatic( Aig_Obj_t * pObj, Aig_Obj_t * pFan ) { ((Aig_Obj_t **)pObj->pData)[pObj->nRefs++] = pFan; }
+
+#define Aig_ObjForEachFanoutStatic( pObj, pFan, i )                        \
+    for ( i = 0; (i < (int)(pObj)->nRefs) && ((pFan) = Aig_ObjFanoutStatic(pObj, i)); i++ )
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate static fanout for all nodes in the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t ** Aig_ManStaticFanoutStart( Aig_Man_t * p )
+{
+    Aig_Obj_t ** ppFanouts, * pObj;
+    int i, nFanouts, nFanoutsAlloc;
+    // allocate fanouts
+    nFanoutsAlloc = 2 * Aig_ManObjNumMax(p) - Aig_ManPiNum(p) - Aig_ManPoNum(p);
+    ppFanouts = ALLOC( Aig_Obj_t *, nFanoutsAlloc );
+    // mark up storage
+    nFanouts = 0;
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        pObj->pData = ppFanouts + nFanouts;
+        nFanouts += pObj->nRefs;  
+        pObj->nRefs = 0;
+    }
+    assert( nFanouts < nFanoutsAlloc ); 
+    // add fanouts
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjChild0(pObj) )
+            Aig_ObjSetFanoutStatic( Aig_ObjFanin0(pObj), pObj );
+        if ( Aig_ObjChild1(pObj) )
+            Aig_ObjSetFanoutStatic( Aig_ObjFanin1(pObj), pObj );
+    }
+    return ppFanouts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the objects reachable from the given object.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManMarkAutonomous_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pFanout;
+    int i;
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    Aig_ObjForEachFanoutStatic( pObj, pFanout, i )
+        Aig_ManMarkAutonomous_rec( p, pFanout );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks with current trav ID nodes reachable from Const1 and PIs.]
+
+  Description [Returns the number of unreachable registers.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManMarkAutonomous( Aig_Man_t * p )
+{
+    Aig_Obj_t ** ppFanouts;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i;
+    // temporarily connect register outputs to register inputs
+    Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
+    {
+        pObjLo->pFanin0 = pObjLi;
+        pObjLi->nRefs = 1;
+    }
+    // mark nodes reachable from Const1 and PIs
+    Aig_ManIncrementTravId( p );
+    ppFanouts = Aig_ManStaticFanoutStart( p );
+    Aig_ManMarkAutonomous_rec( p, Aig_ManConst1(p) );
+    Saig_ManForEachPi( p, pObj, i )
+        Aig_ManMarkAutonomous_rec( p, pObj );
+    free( ppFanouts );
+    // disconnect LIs/LOs and label unreachable registers
+    Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
+    {
+        assert( pObjLo->pFanin0 && pObjLi->nRefs == 1 );
+        pObjLo->pFanin0 = NULL;
+        pObjLi->nRefs = 0;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the cut for forward retiming.]
+
+  Description [Assumes topological ordering of the nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManRetimeForwardOne( Aig_Man_t * p, int * pnRegFixed, int * pnRegMoves )
+{
+    Aig_Man_t * pNew;
+    Vec_Ptr_t * vCut;
+    Aig_Obj_t * pObj, * pFanin;
+    int i;
+    // mark the retimable nodes
+    Saig_ManMarkAutonomous( p );
+    // mark the retimable registers with the fresh trav ID
+    Aig_ManIncrementTravId( p );
+    *pnRegFixed = 0;
+    Saig_ManForEachLo( p, pObj, i )
+        if ( Aig_ObjIsTravIdPrevious(p, pObj) )
+            Aig_ObjSetTravIdCurrent(p, pObj);
+        else
+            (*pnRegFixed)++;
+    // mark all the nodes that can be retimed forward
+    *pnRegMoves = 0;
+    Aig_ManForEachNode( p, pObj, i )
+        if ( Aig_ObjIsTravIdCurrent(p, Aig_ObjFanin0(pObj)) && Aig_ObjIsTravIdCurrent(p, Aig_ObjFanin1(pObj)) )
+        {
+            Aig_ObjSetTravIdCurrent(p, pObj);
+            (*pnRegMoves)++;
+        }
+    // mark the remaining registers
+    Saig_ManForEachLo( p, pObj, i )
+        Aig_ObjSetTravIdCurrent(p, pObj);
+    // find the cut (all such marked objects that fanout into unmarked nodes)
+    vCut = Vec_PtrAlloc( 1000 );
+    Aig_ManIncrementTravId( p );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjIsTravIdPrevious(p, pObj) )
+            continue;
+        pFanin = Aig_ObjFanin0(pObj);
+        if ( pFanin && Aig_ObjIsTravIdPrevious(p, pFanin) )
+        {
+            Vec_PtrPush( vCut, pFanin );
+            Aig_ObjSetTravIdCurrent( p, pFanin );
+        }
+        pFanin = Aig_ObjFanin1(pObj);
+        if ( pFanin && Aig_ObjIsTravIdPrevious(p, pFanin) )
+        {
+            Vec_PtrPush( vCut, pFanin );
+            Aig_ObjSetTravIdCurrent( p, pFanin );
+        }
+    }
+    // finally derive the new manager
+    pNew = Saig_ManRetimeDupForward( p, vCut );
+    Vec_PtrFree( vCut );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the cut for forward retiming.]
+
+  Description [Assumes topological ordering of the nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose )
+{
+    Aig_Man_t * pNew, * pTemp;
+    int i, clk, nRegFixed, nRegMoves = 1;
+    pNew = p;
+    for ( i = 0; i < nMaxIters && nRegMoves > 0; i++ )
+    {
+        clk = clock();
+        pNew = Saig_ManRetimeForwardOne( pTemp = pNew, &nRegFixed, &nRegMoves );
+        if ( fVerbose )
+        {
+            printf( "%2d : And = %6d. Reg = %5d. Unret = %5d. Move = %6d. ", 
+                i + 1, Aig_ManNodeNum(pTemp), Aig_ManRegNum(pTemp), nRegFixed, nRegMoves );
+            PRT( "Time", clock() - clk );
+        }
+        if ( pTemp != p )
+            Aig_ManStop( pTemp );
+    }
+    clk = clock();
+    pNew = Aig_ManReduceLaches( pNew, fVerbose );
+    if ( fVerbose )
+    {
+        PRT( "Register sharing time", clock() - clk );
+    }
+    return pNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c
index c53d6d6b..324d8867 100644
--- a/src/aig/saig/saigRetMin.c
+++ b/src/aig/saig/saigRetMin.c
@@ -617,16 +617,16 @@ Aig_Man_t * Saig_ManRetimeMinAreaBackward( Aig_Man_t * pNew, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
+Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
 {
     Vec_Ptr_t * vCut;
     Aig_Man_t * pNew, * pTemp, * pCopy;
-    int fChanges;
+    int i, fChanges;
     pNew = Aig_ManDup( p );
     // perform several iterations of forward retiming
     fChanges = 0;
     if ( !fBackwardOnly )
-    while ( 1 )
+    for ( i = 0; i < nMaxIters; i++ )
     {
         vCut = Nwk_ManDeriveRetimingCut( pNew, 1, fVerbose );
         if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
@@ -646,7 +646,7 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwar
     // perform several iterations of backward retiming
     fChanges = 0;
     if ( !fForwardOnly && !fInitial )
-    while ( 1 )
+    for ( i = 0; i < nMaxIters; i++ )
     {
         vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose );
         if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
@@ -664,7 +664,7 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwar
         fChanges = 1;
     }
     else if ( !fForwardOnly && fInitial )
-    while ( 1 )
+    for ( i = 0; i < nMaxIters; i++ )
     {
         pCopy = Aig_ManDup( pNew );
         pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose );
diff --git a/src/aig/saig/saigScl.c b/src/aig/saig/saigScl.c
new file mode 100644
index 00000000..b747eff9
--- /dev/null
+++ b/src/aig/saig/saigScl.c
@@ -0,0 +1,74 @@
+/**CFile****************************************************************
+
+  FileName    [saigScl.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Sequential cleanup.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigScl.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Report registers useless for SEC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManReportUselessRegisters( Aig_Man_t * pAig )
+{
+    Aig_Obj_t * pObj, * pDriver;
+    int i, Counter1, Counter2;
+    // set PIO numbers
+    Aig_ManSetPioNumbers( pAig );
+    // check how many POs are driven by a register whose ref count is 1
+    Counter1 = 0;
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        pDriver = Aig_ObjFanin0(pObj);
+        if ( Saig_ObjIsLo(pAig, pDriver) && Aig_ObjRefs(pDriver) == 1 )
+            Counter1++;
+    }
+    // check how many PIs have ref count 1 and drive a register
+    Counter2 = 0;
+    Saig_ManForEachLi( pAig, pObj, i )
+    {
+        pDriver = Aig_ObjFanin0(pObj);
+        if ( Saig_ObjIsPi(pAig, pDriver) && Aig_ObjRefs(pDriver) == 1 )
+            Counter2++;
+    }
+    if ( Counter1 )
+        printf( "Network has %d (out of %d) registers driving POs.\n", Counter1, Saig_ManRegNum(pAig) );
+    if ( Counter2 )
+        printf( "Network has %d (out of %d) registers driven by PIs.\n", Counter2, Saig_ManRegNum(pAig) );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 492fefae..e7896cb1 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -98,6 +98,7 @@ static int Abc_CommandBidec          ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandOrder          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMuxes          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExtSeqDcs      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandReach          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCone           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandNode           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTopmost        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -349,6 +350,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "order",         Abc_CommandOrder,            0 );
     Cmd_CommandAdd( pAbc, "Various",      "muxes",         Abc_CommandMuxes,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "ext_seq_dcs",   Abc_CommandExtSeqDcs,        0 );
+    Cmd_CommandAdd( pAbc, "Various",      "reach",         Abc_CommandReach,            0 );
     Cmd_CommandAdd( pAbc, "Various",      "cone",          Abc_CommandCone,             1 );
     Cmd_CommandAdd( pAbc, "Various",      "node",          Abc_CommandNode,             1 );
     Cmd_CommandAdd( pAbc, "Various",      "topmost",       Abc_CommandTopmost,          1 );
@@ -5605,6 +5607,116 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int nBddMax;
+    int nIterMax;
+    int fPartition;
+    int fReorder;
+    int fVerbose;
+    int c;
+    extern void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nBddMax    = 50000;
+    nIterMax   = 1000;
+    fPartition = 1;
+    fReorder   = 1;
+    fVerbose   = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "BFprvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'B':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nBddMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBddMax < 0 ) 
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nIterMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nIterMax < 0 ) 
+                goto usage;
+            break;
+        case 'p':
+            fPartition ^= 1;
+            break;
+        case 'r':
+            fReorder ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkLatchNum(pNtk) == 0 )
+    {
+        fprintf( stdout, "The current network has no latches.\n" );
+        return 0;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( stdout, "Reachability analysis works only for AIGs (run \"strash\").\n" );
+        return 1;
+    }
+    if ( Abc_NtkPoNum(pNtk) != 1 )
+    {
+        fprintf( stdout, "The sequential miter has more than one output (run \"orpos\").\n" );
+        return 1;
+    }
+    Abc_NtkVerifyUsingBdds( pNtk, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: reach [-BF num] [-prvh]\n" );
+    fprintf( pErr, "\t         verifies sequential miter using BDD-based reachability\n" );
+    fprintf( pErr, "\t-B num : max number of nodes in the intermediate BDDs [default = %d]\n", nBddMax );
+    fprintf( pErr, "\t-F num : max number of reachability iterations [default = %d]\n", nIterMax );
+    fprintf( pErr, "\t-p     : enable partitioned image computation [default = %s]\n", fPartition? "yes": "no" );  
+    fprintf( pErr, "\t-r     : enable dynamic BDD variable reordering [default = %s]\n", fReorder? "yes": "no" );  
+    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -11925,10 +12037,11 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nStepsMax;
     int fFastAlgo;
     int fVerbose;
-    int c;
+    int c, nMaxIters;
     extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
     extern Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
-    extern Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarRetimeMostFwd( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -11940,13 +12053,25 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     fBackwardOnly = 0;
     fInitial = 1;
     nStepsMax = 100000;
-    fFastAlgo = 1;
+    fFastAlgo = 0;
+    nMaxIters = 20;
     fVerbose  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Smfbiavh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NSmfbiavh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nMaxIters = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nMaxIters < 0 ) 
+                goto usage;
+            break;
         case 'S':
             if ( globalUtilOptind >= argc )
             {
@@ -12003,11 +12128,12 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // perform the retiming
     if ( fMinArea )
-        pNtkRes = Abc_NtkDarRetimeMinArea( pNtk, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
+        pNtkRes = Abc_NtkDarRetimeMinArea( pNtk, nMaxIters, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
     else if ( fFastAlgo )
         pNtkRes = Abc_NtkDarRetime( pNtk, nStepsMax, fVerbose );
     else
-        pNtkRes = Abc_NtkDarRetimeF( pNtk, nStepsMax, fVerbose );
+//        pNtkRes = Abc_NtkDarRetimeF( pNtk, nStepsMax, fVerbose );
+        pNtkRes = Abc_NtkDarRetimeMostFwd( pNtk, nMaxIters, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Retiming has failed.\n" );
@@ -12018,12 +12144,13 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dretime [-S num] [-mfbiavh]\n" );
-    fprintf( pErr, "\t         new implementation of min-area retiming\n" );
-    fprintf( pErr, "\t-m     : toggle min-area and most-forward retiming [default = %s]\n", fMinArea? "min-area": "most-fwd" );
+    fprintf( pErr, "usage: dretime [-NS num] [-mfbiavh]\n" );
+    fprintf( pErr, "\t         new implementation of min-area (or most-forward) retiming\n" );
+    fprintf( pErr, "\t-m     : toggle min-area retiming and most-forward retiming [default = %s]\n", fMinArea? "min-area": "most-fwd" );
     fprintf( pErr, "\t-f     : enables forward-only retiming [default = %s]\n", fForwardOnly? "yes": "no" );
     fprintf( pErr, "\t-b     : enables backward-only retiming [default = %s]\n", fBackwardOnly? "yes": "no" );
     fprintf( pErr, "\t-i     : enables init state computation [default = %s]\n", fInitial? "yes": "no" );
+    fprintf( pErr, "\t-N num : the max number of one-frame iterations to perform [default = %d]\n", nMaxIters );
     fprintf( pErr, "\t-S num : the max number of forward retiming steps to perform [default = %d]\n", nStepsMax );
     fprintf( pErr, "\t-a     : enables a fast most-forward algorithm [default = %s]\n", fFastAlgo? "yes": "no" );
     fprintf( pErr, "\t-v     : enables verbose output [default = %s]\n", fVerbose? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 20557fb3..4b1a37c2 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1409,7 +1409,7 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
         Vec_IntFree( pMan->vFlopNums ); 
     pMan->vFlopNums = NULL;
 
-    pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, 0 );
+    pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, fVerbose );
     Aig_ManStop( pTemp );
 
 //    pMan = Aig_ManReduceLaches( pMan, 1 );
@@ -1431,24 +1431,24 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
 {
-    extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return NULL;
+//    Aig_ManReduceLachesCount( pMan );
     if ( pMan->vFlopNums )
         Vec_IntFree( pMan->vFlopNums ); 
     pMan->vFlopNums = NULL;
 
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
-
-    pMan = Saig_ManRetimeMinArea( pTemp = pMan, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
+    pMan = Aig_ManRetimeFrontier( pTemp = pMan, nStepsMax );
     Aig_ManStop( pTemp );
 
+//    pMan = Aig_ManReduceLaches( pMan, 1 );
+//    pMan = Aig_ManConstReduce( pMan, 1 );
+
     pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
     Aig_ManStop( pMan );
     return pNtkAig;
@@ -1465,8 +1465,10 @@ Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBa
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarRetimeMostFwd( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
 {
+    extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nIters, int fVerbose );
+
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
@@ -1477,7 +1479,10 @@ Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
         Vec_IntFree( pMan->vFlopNums ); 
     pMan->vFlopNums = NULL;
 
-    pMan = Aig_ManRetimeFrontier( pTemp = pMan, nStepsMax );
+    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
+    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
+
+    pMan = Saig_ManRetimeForward( pTemp = pMan, nMaxIters, fVerbose );
     Aig_ManStop( pTemp );
 
 //    pMan = Aig_ManReduceLaches( pMan, 1 );
@@ -1499,6 +1504,40 @@ Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
+{
+    extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    if ( pMan->vFlopNums )
+        Vec_IntFree( pMan->vFlopNums ); 
+    pMan->vFlopNums = NULL;
+
+    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
+    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
+
+    pMan = Saig_ManRetimeMinArea( pTemp = pMan, nMaxIters, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
+    Aig_ManStop( pTemp );
+
+    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
 {
 /*
diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c
index 171cbf0a..78e7cf6b 100644
--- a/src/base/abci/abcFpga.c
+++ b/src/base/abci/abcFpga.c
@@ -201,7 +201,7 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pNode, * pNodeNew;
-    int i;//, nDupGates;
+    int i, nDupGates;
     // create the new network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
     // make the mapper point to the new network
@@ -229,9 +229,9 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
     if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
         Abc_NtkDeleteObj( pNodeNew );
     // decouple the PO driver nodes to reduce the number of levels
-//    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
-//    if ( nDupGates && Fpga_ManReadVerbose(pMan) )
-//        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+    if ( nDupGates && Fpga_ManReadVerbose(pMan) )
+        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
     return pNtkNew;
 }
 
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index cf6f88ae..94c7dda8 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -186,7 +186,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pNode, * pNodeNew;
     Vec_Int_t * vCover;
-    int i;//, nDupGates;
+    int i, nDupGates;
     // create the new network
     if ( pIfMan->pPars->fUseBdds || pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
         pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
@@ -223,9 +223,9 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     if ( pIfMan->pPars->fUseBdds )
         Abc_NtkBddReorder( pNtkNew, 0 );
     // decouple the PO driver nodes to reduce the number of levels
-//    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
-//    if ( nDupGates && If_ManReadVerbose(pIfMan) )
-//        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+    if ( nDupGates && pIfMan->pPars->fVerbose )
+        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
     return pNtkNew;
 }
 
diff --git a/src/base/abci/abcReach.c b/src/base/abci/abcReach.c
new file mode 100644
index 00000000..42494b5c
--- /dev/null
+++ b/src/base/abci/abcReach.c
@@ -0,0 +1,313 @@
+/**CFile****************************************************************
+
+  FileName    [abcReach.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Performs reachability analysis.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcReach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the initial state and sets up the variable map.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NtkInitStateVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose )
+{
+    DdNode ** pbVarsX, ** pbVarsY;
+    DdNode * bTemp, * bProd, * bVar;
+    Abc_Obj_t * pLatch;
+    int i;
+
+    // set the variable mapping for Cudd_bddVarMap()
+    pbVarsX = ALLOC( DdNode *, dd->size );
+    pbVarsY = ALLOC( DdNode *, dd->size );
+    bProd = b1;         Cudd_Ref( bProd );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        pbVarsX[i] = dd->vars[ Abc_NtkPiNum(pNtk) + i ];
+        pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
+        // get the initial value of the latch
+        bVar  = Cudd_NotCond( pbVarsX[i], !Abc_LatchIsInit1(pLatch) );
+        bProd = Cudd_bddAnd( dd, bTemp = bProd, bVar );      Cudd_Ref( bProd );
+        Cudd_RecursiveDeref( dd, bTemp ); 
+    }
+    Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Abc_NtkLatchNum(pNtk) );
+    FREE( pbVarsX );
+    FREE( pbVarsY );
+
+    Cudd_Deref( bProd );
+    return bProd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode ** Abc_NtkCreatePartitions( DdManager * dd, Abc_Ntk_t * pNtk, int fReorder, int fVerbose )
+{
+    DdNode ** pbParts;
+    DdNode * bVar;
+    Abc_Obj_t * pNode;
+    int i;
+
+    // extand the BDD manager to represent NS variables
+    assert( dd->size == Abc_NtkCiNum(pNtk) );
+    Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + Abc_NtkLatchNum(pNtk) - 1 );
+
+    // enable reordering
+    if ( fReorder )
+        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+    else
+        Cudd_AutodynDisable( dd );
+
+    // compute the transition relation
+    pbParts = ALLOC( DdNode *, Abc_NtkLatchNum(pNtk) );
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+    {
+        bVar  = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
+        pbParts[i] = Cudd_bddXnor( dd, bVar, Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) );  Cudd_Ref( pbParts[i] );
+    }
+    // free the global BDDs
+    Abc_NtkFreeGlobalBdds( pNtk, 0 );
+
+    // reorder and disable reordering
+    if ( fReorder )
+    {
+        if ( fVerbose )
+            fprintf( stdout, "BDD nodes in the partitions before reordering %d.\n", Cudd_SharingSize(pbParts,Abc_NtkLatchNum(pNtk)) );
+        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
+        Cudd_AutodynDisable( dd );
+        if ( fVerbose )
+            fprintf( stdout, "BDD nodes in the partitions after reordering %d.\n", Cudd_SharingSize(pbParts,Abc_NtkLatchNum(pNtk)) );
+    }
+    return pbParts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the set of unreachable states.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NtkComputeReachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode ** pbParts, DdNode * bInitial, DdNode * bOutput, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
+{
+    int fInternalReorder = 0;
+    Extra_ImageTree_t * pTree;
+    Extra_ImageTree2_t * pTree2;
+    DdNode * bReached, * bCubeCs;
+    DdNode * bCurrent, * bNext, * bTemp;
+    DdNode ** pbVarsY;
+    Abc_Obj_t * pLatch;
+    int i, nIters, nBddSize;
+    int nThreshold = 10000;
+
+    // collect the NS variables
+    // set the variable mapping for Cudd_bddVarMap()
+    pbVarsY = ALLOC( DdNode *, dd->size );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
+
+    // start the image computation
+    bCubeCs  = Extra_bddComputeRangeCube( dd, Abc_NtkPiNum(pNtk), Abc_NtkCiNum(pNtk) );    Cudd_Ref( bCubeCs );
+    if ( fPartition )
+        pTree = Extra_bddImageStart( dd, bCubeCs, Abc_NtkLatchNum(pNtk), pbParts, Abc_NtkLatchNum(pNtk), pbVarsY, fVerbose );
+    else
+        pTree2 = Extra_bddImageStart2( dd, bCubeCs, Abc_NtkLatchNum(pNtk), pbParts, Abc_NtkLatchNum(pNtk), pbVarsY, fVerbose );
+    free( pbVarsY );
+    Cudd_RecursiveDeref( dd, bCubeCs );
+
+    // perform reachability analisys
+    bCurrent = bInitial;   Cudd_Ref( bCurrent );
+    bReached = bInitial;   Cudd_Ref( bReached );
+    for ( nIters = 1; nIters <= nIterMax; nIters++ )
+    {
+        // compute the next states
+        if ( fPartition )
+            bNext = Extra_bddImageCompute( pTree, bCurrent );           
+        else
+            bNext = Extra_bddImageCompute2( pTree2, bCurrent );         
+        Cudd_Ref( bNext );
+        Cudd_RecursiveDeref( dd, bCurrent );
+        // remap these states into the current state vars
+        bNext = Cudd_bddVarMap( dd, bTemp = bNext );                    Cudd_Ref( bNext );
+        Cudd_RecursiveDeref( dd, bTemp );
+        // check if there are any new states
+        if ( Cudd_bddLeq( dd, bNext, bReached ) )
+            break;
+        // check the BDD size
+        nBddSize = Cudd_DagSize(bNext);
+        if ( nBddSize > nBddMax )
+            break;
+        // check the result
+        if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(bOutput) ) )
+        {
+            printf( "The miter is proved REACHABLE in %d iterations.  ", nIters );
+            Cudd_RecursiveDeref( dd, bReached );
+            bReached = NULL;
+            break;
+        }
+        // get the new states
+        bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) );        Cudd_Ref( bCurrent );
+        // minimize the new states with the reached states
+//        bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
+//        Cudd_RecursiveDeref( dd, bTemp );
+        // add to the reached states
+        bReached = Cudd_bddOr( dd, bTemp = bReached, bNext );           Cudd_Ref( bReached );
+        Cudd_RecursiveDeref( dd, bTemp );
+        Cudd_RecursiveDeref( dd, bNext );
+        if ( fVerbose )
+            fprintf( stdout, "Iteration = %3d. BDD = %5d. ", nIters, nBddSize );
+        if ( fInternalReorder && fReorder && nBddSize > nThreshold )
+        {
+            if ( fVerbose )
+                fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) );
+            Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
+            Cudd_AutodynDisable( dd );
+            if ( fVerbose )
+                fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) );
+            nThreshold *= 2;
+        }
+        if ( fVerbose )
+            fprintf( stdout, "\r" );
+    }
+    Cudd_RecursiveDeref( dd, bNext );
+    // undo the image tree
+    if ( fPartition )
+        Extra_bddImageTreeDelete( pTree );
+    else
+        Extra_bddImageTreeDelete2( pTree2 );
+    if ( bReached == NULL )
+        return NULL;
+    // report the stats
+    if ( fVerbose )
+    {
+        double nMints = Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) );
+        if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
+            fprintf( stdout, "Reachability analysis is stopped after %d iterations.\n", nIters );
+        else
+            fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
+        fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Abc_NtkLatchNum(pNtk)) );
+        fflush( stdout );
+    }
+//PRB( dd, bReached );
+    Cudd_Deref( bReached );
+    if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
+         printf( "Verified ONLY FOR STATES REACHED in %d iterations. \n", nIters );
+    printf( "The miter is proved unreachable in %d iteration.  ", nIters );
+    return bReached;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs reachability to see if any .]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
+{
+    DdManager * dd;
+    DdNode ** pbParts;
+    DdNode * bOutput, * bReached, * bInitial;
+    int i, clk = clock();
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( Abc_NtkPoNum(pNtk) == 1 );
+    assert( Abc_ObjFanoutNum(Abc_NtkPo(pNtk,0)) == 0 ); // PO should go first
+
+    // compute the global BDDs of the latches
+    dd = Abc_NtkBuildGlobalBdds( pNtk, nBddMax, 1, fReorder, fVerbose );    
+    if ( dd == NULL )
+    {
+        printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax );
+        return;
+    }
+    if ( fVerbose )
+        printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+
+    // save the output BDD
+    bOutput = Abc_ObjGlobalBdd(Abc_NtkPo(pNtk,0)); Cudd_Ref( bOutput );
+
+    // create partitions
+    pbParts = Abc_NtkCreatePartitions( dd, pNtk, fReorder, fVerbose );
+
+    // create the initial state and the variable map
+    bInitial  = Abc_NtkInitStateVarMap( dd, pNtk, fVerbose );  Cudd_Ref( bInitial );
+
+    // check the result
+    if ( !Cudd_bddLeq( dd, bInitial, Cudd_Not(bOutput) ) )
+        printf( "The miter is proved REACHABLE in the initial state.  " );
+    else
+    {
+        // compute the reachable states
+        bReached = Abc_NtkComputeReachable( dd, pNtk, pbParts, bInitial, bOutput, nBddMax, nIterMax, fPartition, fReorder, fVerbose ); 
+        if ( bReached != NULL )
+        {
+            Cudd_Ref( bReached );
+            Cudd_RecursiveDeref( dd, bReached );
+        }
+    }
+
+    // cleanup
+    Cudd_RecursiveDeref( dd, bOutput );
+    Cudd_RecursiveDeref( dd, bInitial );
+    for ( i = 0; i < Abc_NtkLatchNum(pNtk); i++ )
+        Cudd_RecursiveDeref( dd, pbParts[i] );
+    free( pbParts );
+    Extra_StopManager( dd );
+
+    // report the runtime
+    PRT( "Time", clock() - clk );
+    fflush( stdout );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 716f1618..ca2f2501 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -39,6 +39,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcQuant.c \
     src/base/abci/abcRec.c \
     src/base/abci/abcReconv.c \
+    src/base/abci/abcReach.c \
     src/base/abci/abcRefactor.c \
     src/base/abci/abcRenode.c \
     src/base/abci/abcReorder.c \
diff --git a/src/bdd/cas/casCore.c b/src/bdd/cas/casCore.c
index 579235b1..84d1e97b 100644
--- a/src/bdd/cas/casCore.c
+++ b/src/bdd/cas/casCore.c
@@ -52,7 +52,7 @@ DdNode * Cudd_bddTransferPermute( DdManager * ddSource, DdManager * ddDestinatio
 ////////////////////////////////////////////////////////////////////////
 
 #define PRD(p)       printf( "\nDECOMPOSITION TREE:\n\n" ); PrintDecEntry( (p), 0 ) 
-#define PRB(f)       printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
+#define PRB_(f)       printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
 #define PRK(f,n)     Cudd_PrintKMap(stdout,dd,(f),Cudd_Not(f),(n),NULL,0); printf( "K-map for function" #f "\n\n" )
 #define PRK2(f,g,n)  Cudd_PrintKMap(stdout,dd,(f),(g),(n),NULL,0); printf( "K-map for function <" #f ", " #g ">\n\n" ) 
 
diff --git a/src/bdd/cas/casDec.c b/src/bdd/cas/casDec.c
index a1eb5f36..3435f30d 100644
--- a/src/bdd/cas/casDec.c
+++ b/src/bdd/cas/casDec.c
@@ -94,7 +94,7 @@ long s_EncComputeTime;
 ///                      debugging macros                            ///
 ////////////////////////////////////////////////////////////////////////
 
-#define PRB(f)       printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
+#define PRB_(f)       printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
 #define PRK(f,n)     Cudd_PrintKMap(stdout,dd,(f),Cudd_Not(f),(n),NULL,0); printf( "K-map for function" #f "\n\n" )
 #define PRK2(f,g,n)  Cudd_PrintKMap(stdout,dd,(f),(g),(n),NULL,0); printf( "K-map for function <" #f ", " #g ">\n\n" ) 
 
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/pcm/module.make
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/ply/module.make
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 8f86fc32..9870c3d0 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -118,6 +118,10 @@ typedef unsigned long long uint64;
 #define PRTP(a,t,T)  printf("%s = ", (a)); printf("%6.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0)
 #endif
 
+#ifndef PRB
+#define PRB(dd,f)       printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
+#endif
+
 /*===========================================================================*/
 /*     Various Utilities                                                     */
 /*===========================================================================*/
@@ -162,6 +166,26 @@ extern int          Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** p
 /* find the profile of a DD (the number of edges crossing each level) */
 extern int          Extra_ProfileWidth( DdManager * dd, DdNode * F, int * Profile, int CutLevel );
 
+/*=== extraBddImage.c ================================================================*/
+
+typedef struct Extra_ImageTree_t_  Extra_ImageTree_t;
+extern Extra_ImageTree_t * Extra_bddImageStart( 
+    DdManager * dd, DdNode * bCare,
+    int nParts, DdNode ** pbParts,
+    int nVars, DdNode ** pbVars, int fVerbose );
+extern DdNode *    Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare );
+extern void        Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree );
+extern DdNode *    Extra_bddImageRead( Extra_ImageTree_t * pTree );
+
+typedef struct Extra_ImageTree2_t_  Extra_ImageTree2_t;
+extern Extra_ImageTree2_t * Extra_bddImageStart2( 
+    DdManager * dd, DdNode * bCare,
+    int nParts, DdNode ** pbParts,
+    int nVars, DdNode ** pbVars, int fVerbose );
+extern DdNode *    Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare );
+extern void        Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree );
+extern DdNode *    Extra_bddImageRead2( Extra_ImageTree2_t * pTree );
+
 /*=== extraBddMisc.c ========================================================*/
 
 extern DdNode *     Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute );
@@ -190,6 +214,7 @@ extern DdNode *     Extra_bddCreateOr( DdManager * dd, int nVars );
 extern DdNode *     Extra_bddCreateExor( DdManager * dd, int nVars );
 extern DdNode *     Extra_zddPrimes( DdManager * dd, DdNode * F );
 extern void         Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut );
+extern DdNode *     Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars );
 
 /*=== extraBddKmap.c ================================================================*/
 
diff --git a/src/misc/extra/extraBddImage.c b/src/misc/extra/extraBddImage.c
new file mode 100644
index 00000000..d21cfe23
--- /dev/null
+++ b/src/misc/extra/extraBddImage.c
@@ -0,0 +1,1157 @@
+/**CFile****************************************************************
+
+  FileName    [extraBddImage.c]
+
+  PackageName [extra]
+
+  Synopsis    [Various reusable software utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2003.]
+
+  Revision    [$Id: extraBddImage.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+
+/* 
+    The ideas implemented in this file are inspired by the paper:
+    Pankaj Chauhan, Edmund Clarke, Somesh Jha, Jim Kukula, Tom Shiple, 
+    Helmut Veith, Dong Wang. Non-linear Quantification Scheduling in 
+    Image Computation. ICCAD, 2001.
+*/
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+typedef struct Extra_ImageNode_t_  Extra_ImageNode_t;
+typedef struct Extra_ImagePart_t_  Extra_ImagePart_t;
+typedef struct Extra_ImageVar_t_   Extra_ImageVar_t;
+
+struct Extra_ImageTree_t_
+{
+    Extra_ImageNode_t * pRoot;      // the root of quantification tree
+    Extra_ImageNode_t * pCare;      // the leaf node with the care set
+    DdNode *            bCareSupp;  // the cube to quantify from the care
+    int                 fVerbose;   // the verbosity flag
+    int                 nNodesMax;  // the max number of nodes in one iter
+    int                 nNodesMaxT; // the overall max number of nodes
+    int                 nIter;      // the number of iterations with this tree
+};
+
+struct Extra_ImageNode_t_
+{
+    DdManager *         dd;         // the manager 
+    DdNode *            bCube;      // the cube to quantify
+    DdNode *            bImage;     // the partial image
+    Extra_ImageNode_t * pNode1;     // the first branch
+    Extra_ImageNode_t * pNode2;     // the second branch
+    Extra_ImagePart_t * pPart;      // the partition (temporary)
+};
+
+struct Extra_ImagePart_t_
+{
+    DdNode *            bFunc;      // the partition
+    DdNode *            bSupp;      // the support of this partition
+    int                 nNodes;     // the number of BDD nodes
+    short               nSupp;      // the number of support variables
+    short               iPart;      // the number of this partition
+};
+
+struct Extra_ImageVar_t_
+{
+    int                 iNum;       // the BDD index of this variable
+    DdNode *            bParts;     // the partition numbers
+    int                 nParts;     // the number of partitions
+};
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticStart*************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+static Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd,
+    int nParts, DdNode ** pbParts, DdNode * bCare );
+static Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd,
+    int nParts, Extra_ImagePart_t ** pParts,
+    int nVars, DdNode ** pbVarsNs );
+static Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd, 
+    int nParts, Extra_ImagePart_t ** pParts, 
+    int nVars,  Extra_ImageVar_t ** pVars );
+static void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode );
+static int Extra_BuildTreeNode( DdManager * dd, 
+    int nNodes, Extra_ImageNode_t ** pNodes, 
+    int nVars,  Extra_ImageVar_t ** pVars );
+static Extra_ImageNode_t * Extra_MergeTopNodes( DdManager * dd, 
+    int nNodes, Extra_ImageNode_t ** pNodes );
+static void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode );
+static void Extra_bddImageCompute_rec( Extra_ImageTree_t * pTree, Extra_ImageNode_t * pNode );
+static int Extra_FindBestVariable( DdManager * dd,
+    int nNodes, Extra_ImageNode_t ** pNodes, 
+    int nVars,  Extra_ImageVar_t ** pVars );
+static void Extra_FindBestPartitions( DdManager * dd, DdNode * bParts, 
+    int nNodes, Extra_ImageNode_t ** pNodes, 
+    int * piNode1, int * piNode2 );
+static Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube,
+    Extra_ImageNode_t * pNode1, Extra_ImageNode_t * pNode2 );
+
+static void Extra_bddImagePrintLatchDependency( DdManager * dd, DdNode * bCare,
+    int nParts, DdNode ** pbParts,
+    int nVars, DdNode ** pbVars );
+static void Extra_bddImagePrintLatchDependencyOne( DdManager * dd, DdNode * bFunc, 
+    DdNode * bVarsCs, DdNode * bVarsNs, int iPart );
+
+static void Extra_bddImagePrintTree( Extra_ImageTree_t * pTree );
+static void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int nOffset );
+
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the image computation using tree-based scheduling.]
+
+  Description [This procedure starts the image computation. It uses
+  the given care set to test-run the image computation and creates the 
+  quantification tree by scheduling variable quantifications. The tree can 
+  be used to compute images for other care sets without rescheduling.
+  In this case, Extra_bddImageCompute() should be called.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Extra_ImageTree_t * Extra_bddImageStart( 
+    DdManager * dd, DdNode * bCare, // the care set
+    int nParts, DdNode ** pbParts,  // the partitions for image computation
+    int nVars, DdNode ** pbVars, int fVerbose )   // the NS and parameter variables (not quantified!)
+{
+    Extra_ImageTree_t * pTree;
+    Extra_ImagePart_t ** pParts;
+    Extra_ImageVar_t ** pVars;
+    Extra_ImageNode_t ** pNodes;
+    int v;
+
+    if ( fVerbose && dd->size <= 80 )
+        Extra_bddImagePrintLatchDependency( dd, bCare, nParts, pbParts, nVars, pbVars );
+
+    // create variables, partitions and leaf nodes
+    pParts = Extra_CreateParts( dd, nParts, pbParts, bCare );
+    pVars  = Extra_CreateVars( dd, nParts + 1, pParts, nVars, pbVars );
+    pNodes = Extra_CreateNodes( dd, nParts + 1, pParts, dd->size, pVars );
+    
+    // create the tree
+    pTree = ALLOC( Extra_ImageTree_t, 1 );
+    memset( pTree, 0, sizeof(Extra_ImageTree_t) );
+    pTree->pCare = pNodes[nParts];
+    pTree->fVerbose = fVerbose;
+
+    // process the nodes
+    while ( Extra_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars ) );
+
+    // make sure the variables are gone
+    for ( v = 0; v < dd->size; v++ )
+        assert( pVars[v] == NULL );
+    FREE( pVars );
+
+    // merge the topmost nodes
+    while ( (pTree->pRoot = Extra_MergeTopNodes( dd, nParts + 1, pNodes )) == NULL );
+
+    // make sure the nodes are gone
+    for ( v = 0; v < nParts + 1; v++ )
+        assert( pNodes[v] == NULL );
+    FREE( pNodes );
+
+//    if ( fVerbose )
+//        Extra_bddImagePrintTree( pTree );
+
+    // set the support of the care set
+    pTree->bCareSupp = Cudd_Support( dd, bCare );  Cudd_Ref( pTree->bCareSupp );
+
+    // clean the partitions
+    Extra_DeleteParts_rec( pTree->pRoot );
+    FREE( pParts );
+    return pTree;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the image.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare )
+{
+    DdManager * dd = pTree->pCare->dd;
+    DdNode * bSupp, * bRem;
+
+    pTree->nIter++;
+
+    // make sure the supports are okay
+    bSupp = Cudd_Support( dd, bCare );        Cudd_Ref( bSupp );
+    if ( bSupp != pTree->bCareSupp )
+    {
+        bRem = Cudd_bddExistAbstract( dd, bSupp, pTree->bCareSupp );  Cudd_Ref( bRem );
+        if ( bRem != b1 )
+        {
+printf( "Original care set support: " );
+PRB( dd, pTree->bCareSupp );
+printf( "Current care set support: " );
+PRB( dd, bSupp );
+            Cudd_RecursiveDeref( dd, bSupp );
+            Cudd_RecursiveDeref( dd, bRem );
+            printf( "The care set depends on some vars that were not in the care set during scheduling.\n" );
+            return NULL;
+        }
+        Cudd_RecursiveDeref( dd, bRem );
+    }
+    Cudd_RecursiveDeref( dd, bSupp );
+
+    // remove the previous image
+    Cudd_RecursiveDeref( dd, pTree->pCare->bImage );
+    pTree->pCare->bImage = bCare;   Cudd_Ref( bCare );
+
+    // compute the image
+    pTree->nNodesMax = 0;
+    Extra_bddImageCompute_rec( pTree, pTree->pRoot );
+    if ( pTree->nNodesMaxT < pTree->nNodesMax )
+        pTree->nNodesMaxT = pTree->nNodesMax;
+
+//    if ( pTree->fVerbose )
+//        printf( "Iter %2d : Max nodes = %5d.\n", pTree->nIter, pTree->nNodesMax );
+    return pTree->pRoot->bImage;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Delete the tree.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree )
+{
+    if ( pTree->bCareSupp )
+        Cudd_RecursiveDeref( pTree->pRoot->dd, pTree->bCareSupp );
+    Extra_bddImageTreeDelete_rec( pTree->pRoot );
+    FREE( pTree );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the image from the tree.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Extra_bddImageRead( Extra_ImageTree_t * pTree )
+{
+    return pTree->pRoot->bImage;
+}
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static Functions                                            */
+/*---------------------------------------------------------------------------*/
+
+/**Function*************************************************************
+
+  Synopsis    [Creates partitions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd,
+    int nParts, DdNode ** pbParts, DdNode * bCare )
+{
+    Extra_ImagePart_t ** pParts;
+    int i;
+
+    // start the partitions
+    pParts = ALLOC( Extra_ImagePart_t *, nParts + 1 );
+    // create structures for each variable
+    for ( i = 0; i < nParts; i++ )
+    {
+        pParts[i] = ALLOC( Extra_ImagePart_t, 1 );
+        pParts[i]->bFunc  = pbParts[i];                           Cudd_Ref( pParts[i]->bFunc );
+        pParts[i]->bSupp  = Cudd_Support( dd, pParts[i]->bFunc ); Cudd_Ref( pParts[i]->bSupp );
+        pParts[i]->nSupp  = Extra_bddSuppSize( dd, pParts[i]->bSupp );
+        pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
+        pParts[i]->iPart  = i;
+    }
+    // add the care set as the last partition
+    pParts[nParts] = ALLOC( Extra_ImagePart_t, 1 );
+    pParts[nParts]->bFunc = bCare;                                     Cudd_Ref( pParts[nParts]->bFunc );
+    pParts[nParts]->bSupp = Cudd_Support( dd, pParts[nParts]->bFunc ); Cudd_Ref( pParts[nParts]->bSupp );
+    pParts[nParts]->nSupp = Extra_bddSuppSize( dd, pParts[nParts]->bSupp );
+    pParts[nParts]->nNodes = Cudd_DagSize( pParts[nParts]->bFunc );
+    pParts[nParts]->iPart  = nParts;
+    return pParts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd,
+    int nParts, Extra_ImagePart_t ** pParts,
+    int nVars, DdNode ** pbVars )
+{
+    Extra_ImageVar_t ** pVars;
+    DdNode ** pbFuncs;
+    DdNode * bCubeNs, * bSupp, * bParts, * bTemp, * bSuppTemp;
+    int nVarsTotal, iVar, p, Counter;
+
+    // put all the functions into one array
+    pbFuncs = ALLOC( DdNode *, nParts );
+    for ( p = 0; p < nParts; p++ )
+        pbFuncs[p] = pParts[p]->bSupp;
+    bSupp = Cudd_VectorSupport( dd, pbFuncs, nParts );  Cudd_Ref( bSupp );
+    FREE( pbFuncs );
+
+    // remove the NS vars
+    bCubeNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars );        Cudd_Ref( bCubeNs );
+    bSupp = Cudd_bddExistAbstract( dd, bTemp = bSupp, bCubeNs );     Cudd_Ref( bSupp );
+    Cudd_RecursiveDeref( dd, bTemp );
+    Cudd_RecursiveDeref( dd, bCubeNs );
+
+    // get the number of I and CS variables to be quantified
+    nVarsTotal = Extra_bddSuppSize( dd, bSupp );
+
+    // start the variables
+    pVars = ALLOC( Extra_ImageVar_t *, dd->size );
+    memset( pVars, 0, sizeof(Extra_ImageVar_t *) * dd->size );
+    // create structures for each variable
+    for ( bSuppTemp = bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
+    {
+        iVar = bSuppTemp->index;
+        pVars[iVar] = ALLOC( Extra_ImageVar_t, 1 );
+        pVars[iVar]->iNum = iVar;
+        // collect all the parts this var belongs to
+        Counter = 0;
+        bParts = b1; Cudd_Ref( bParts );
+        for ( p = 0; p < nParts; p++ )
+            if ( Cudd_bddLeq( dd, pParts[p]->bSupp, dd->vars[bSuppTemp->index] ) )
+            {
+                bParts = Cudd_bddAnd( dd, bTemp = bParts, dd->vars[p] );  Cudd_Ref( bParts );
+                Cudd_RecursiveDeref( dd, bTemp );
+                Counter++;
+            }
+        pVars[iVar]->bParts = bParts; // takes ref
+        pVars[iVar]->nParts = Counter;
+    }
+    Cudd_RecursiveDeref( dd, bSupp );
+    return pVars;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd, 
+    int nParts, Extra_ImagePart_t ** pParts, 
+    int nVars,  Extra_ImageVar_t ** pVars )
+{
+    Extra_ImageNode_t ** pNodes;
+    Extra_ImageNode_t * pNode;
+    DdNode * bTemp;
+    int i, v, iPart;
+/*
+    DdManager *         dd;       // the manager 
+    DdNode *            bCube;    // the cube to quantify
+    DdNode *            bImage;   // the partial image
+    Extra_ImageNode_t * pNode1;   // the first branch
+    Extra_ImageNode_t * pNode2;   // the second branch
+    Extra_ImagePart_t * pPart;    // the partition (temporary)
+*/
+    // start the partitions
+    pNodes = ALLOC( Extra_ImageNode_t *, nParts );
+    // create structures for each leaf nodes
+    for ( i = 0; i < nParts; i++ )
+    {
+        pNodes[i] = ALLOC( Extra_ImageNode_t, 1 );
+        memset( pNodes[i], 0, sizeof(Extra_ImageNode_t) );
+        pNodes[i]->dd    = dd;
+        pNodes[i]->pPart = pParts[i];
+    }
+    // find the quantification cubes for each leaf node
+    for ( v = 0; v < nVars; v++ )
+    {
+        if ( pVars[v] == NULL )
+            continue;
+        assert( pVars[v]->nParts > 0 );
+        if ( pVars[v]->nParts > 1 )
+            continue;
+        iPart = pVars[v]->bParts->index;
+        if ( pNodes[iPart]->bCube == NULL )
+        {
+            pNodes[iPart]->bCube = dd->vars[v];   
+            Cudd_Ref( dd->vars[v] );
+        }
+        else
+        {
+            pNodes[iPart]->bCube = Cudd_bddAnd( dd, bTemp = pNodes[iPart]->bCube, dd->vars[v] );  
+            Cudd_Ref( pNodes[iPart]->bCube );
+            Cudd_RecursiveDeref( dd, bTemp );
+        }
+        // remove these  variables
+        Cudd_RecursiveDeref( dd, pVars[v]->bParts );
+        FREE( pVars[v] );
+    }
+
+    // assign the leaf node images
+    for ( i = 0; i < nParts; i++ )
+    {
+        pNode = pNodes[i];
+        if ( pNode->bCube )
+        {
+            // update the partition
+            pParts[i]->bFunc = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bFunc, pNode->bCube );
+            Cudd_Ref( pParts[i]->bFunc );
+            Cudd_RecursiveDeref( dd, bTemp );
+            // update the support the partition
+            pParts[i]->bSupp = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bSupp, pNode->bCube ); 
+            Cudd_Ref( pParts[i]->bSupp );
+            Cudd_RecursiveDeref( dd, bTemp );
+            // update the numbers
+            pParts[i]->nSupp  = Extra_bddSuppSize( dd, pParts[i]->bSupp );
+            pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
+            // get rid of the cube
+            // save the last (care set) quantification cube
+            if ( i < nParts - 1 )
+            {
+                Cudd_RecursiveDeref( dd, pNode->bCube );
+                pNode->bCube = NULL;
+            }
+        }
+        // copy the function
+        pNode->bImage = pParts[i]->bFunc;   Cudd_Ref( pNode->bImage );
+    }
+/*
+    for ( i = 0; i < nParts; i++ )
+    {
+        pNode = pNodes[i];
+PRB( dd, pNode->bCube );
+PRB( dd, pNode->pPart->bFunc );
+PRB( dd, pNode->pPart->bSupp );
+printf( "\n" );
+    }
+*/
+    return pNodes;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Delete the partitions from the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode )
+{
+    Extra_ImagePart_t * pPart;
+    if ( pNode->pNode1 )
+        Extra_DeleteParts_rec( pNode->pNode1 );
+    if ( pNode->pNode2 )
+        Extra_DeleteParts_rec( pNode->pNode2 );
+    pPart = pNode->pPart;
+    Cudd_RecursiveDeref( pNode->dd, pPart->bFunc );
+    Cudd_RecursiveDeref( pNode->dd, pPart->bSupp );
+    FREE( pNode->pPart );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Delete the partitions from the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode )
+{
+    if ( pNode->pNode1 )
+        Extra_bddImageTreeDelete_rec( pNode->pNode1 );
+    if ( pNode->pNode2 )
+        Extra_bddImageTreeDelete_rec( pNode->pNode2 );
+    if ( pNode->bCube )
+        Cudd_RecursiveDeref( pNode->dd, pNode->bCube );
+    if ( pNode->bImage )
+        Cudd_RecursiveDeref( pNode->dd, pNode->bImage );
+    assert( pNode->pPart == NULL );
+    FREE( pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recompute the image.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_bddImageCompute_rec( Extra_ImageTree_t * pTree, Extra_ImageNode_t * pNode )
+{
+    DdManager * dd = pNode->dd;
+    DdNode * bTemp;
+    int nNodes;
+
+    // trivial case
+    if ( pNode->pNode1 == NULL )
+    {
+        if ( pNode->bCube )
+        {
+            pNode->bImage = Cudd_bddExistAbstract( dd, bTemp = pNode->bImage, pNode->bCube ); 
+            Cudd_Ref( pNode->bImage );
+            Cudd_RecursiveDeref( dd, bTemp );
+        }
+        return;
+    }
+
+    // compute the children
+    if ( pNode->pNode1 )
+        Extra_bddImageCompute_rec( pTree, pNode->pNode1 );
+    if ( pNode->pNode2 )
+        Extra_bddImageCompute_rec( pTree, pNode->pNode2 );
+
+    // clean the old image
+    if ( pNode->bImage )
+        Cudd_RecursiveDeref( dd, pNode->bImage );
+    pNode->bImage = NULL;
+
+    // compute the new image
+    if ( pNode->bCube )
+        pNode->bImage = Cudd_bddAndAbstract( dd, 
+            pNode->pNode1->bImage, pNode->pNode2->bImage, pNode->bCube );
+    else
+        pNode->bImage = Cudd_bddAnd( dd, pNode->pNode1->bImage, pNode->pNode2->bImage );
+    Cudd_Ref( pNode->bImage );
+
+    if ( pTree->fVerbose )
+    {
+        nNodes = Cudd_DagSize( pNode->bImage );
+        if ( pTree->nNodesMax < nNodes )
+            pTree->nNodesMax = nNodes;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Builds the tree.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_BuildTreeNode( DdManager * dd, 
+    int nNodes, Extra_ImageNode_t ** pNodes, 
+    int nVars,  Extra_ImageVar_t ** pVars )
+{
+    Extra_ImageNode_t * pNode1, * pNode2;
+    Extra_ImageVar_t * pVar;
+    Extra_ImageNode_t * pNode;
+    DdNode * bCube, * bTemp, * bSuppTemp, * bParts;
+    int iNode1, iNode2;
+    int iVarBest, nSupp, v;
+
+    // find the best variable
+    iVarBest = Extra_FindBestVariable( dd, nNodes, pNodes, nVars, pVars );
+    if ( iVarBest == -1 )
+        return 0;
+
+    pVar = pVars[iVarBest];
+
+    // this var cannot appear in one partition only
+    nSupp = Extra_bddSuppSize( dd, pVar->bParts );
+    assert( nSupp == pVar->nParts );
+    assert( nSupp != 1 );
+
+    // if it appears in only two partitions, quantify it
+    if ( pVar->nParts == 2 )
+    {
+        // get the nodes
+        iNode1 = pVar->bParts->index;
+        iNode2 = cuddT(pVar->bParts)->index;
+        pNode1 = pNodes[iNode1];
+        pNode2 = pNodes[iNode2];
+
+        // get the quantification cube
+        bCube = dd->vars[pVar->iNum];    Cudd_Ref( bCube );
+        // add the variables that appear only in these partitions
+        for ( v = 0; v < nVars; v++ )
+            if ( pVars[v] && v != iVarBest && pVars[v]->bParts == pVars[iVarBest]->bParts )
+            {
+                // add this var
+                bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[pVars[v]->iNum] );   Cudd_Ref( bCube );
+                Cudd_RecursiveDeref( dd, bTemp );
+                // clean this var
+                Cudd_RecursiveDeref( dd, pVars[v]->bParts );
+                FREE( pVars[v] );
+            }
+        // clean the best var
+        Cudd_RecursiveDeref( dd, pVars[iVarBest]->bParts );
+        FREE( pVars[iVarBest] );
+
+        // combines two nodes
+        pNode = Extra_CombineTwoNodes( dd, bCube, pNode1, pNode2 );
+        Cudd_RecursiveDeref( dd, bCube );
+    }
+    else // if ( pVar->nParts > 2 )
+    {
+        // find two smallest BDDs that have this var
+        Extra_FindBestPartitions( dd, pVar->bParts, nNodes, pNodes, &iNode1, &iNode2 );
+        pNode1 = pNodes[iNode1];
+        pNode2 = pNodes[iNode2];
+
+        // it is not possible that a var appears only in these two
+        // otherwise, it would have a different cost
+        bParts = Cudd_bddAnd( dd, dd->vars[iNode1], dd->vars[iNode2] ); Cudd_Ref( bParts );
+        for ( v = 0; v < nVars; v++ )
+            if ( pVars[v] && pVars[v]->bParts == bParts )
+                assert( 0 );
+        Cudd_RecursiveDeref( dd, bParts );
+
+        // combines two nodes
+        pNode = Extra_CombineTwoNodes( dd, b1, pNode1, pNode2 );
+    }
+
+    // clean the old nodes
+    pNodes[iNode1] = pNode;
+    pNodes[iNode2] = NULL;
+    
+    // update the variables that appear in pNode[iNode2]
+    for ( bSuppTemp = pNode2->pPart->bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
+    {
+        pVar = pVars[bSuppTemp->index];
+        if ( pVar == NULL ) // this variable is not be quantified
+            continue;
+        // quantify this var
+        assert( Cudd_bddLeq( dd, pVar->bParts, dd->vars[iNode2] ) );
+        pVar->bParts = Cudd_bddExistAbstract( dd, bTemp = pVar->bParts, dd->vars[iNode2] ); Cudd_Ref( pVar->bParts );
+        Cudd_RecursiveDeref( dd, bTemp );
+        // add the new var
+        pVar->bParts = Cudd_bddAnd( dd, bTemp = pVar->bParts, dd->vars[iNode1] ); Cudd_Ref( pVar->bParts );
+        Cudd_RecursiveDeref( dd, bTemp );
+        // update the score
+        pVar->nParts = Extra_bddSuppSize( dd, pVar->bParts );
+    }
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Merges the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Extra_ImageNode_t * Extra_MergeTopNodes(
+    DdManager * dd, int nNodes, Extra_ImageNode_t ** pNodes )
+{
+    Extra_ImageNode_t * pNode;
+    int n1 = -1, n2 = -1, n;
+
+    // find the first and the second non-empty spots
+    for ( n = 0; n < nNodes; n++ )
+        if ( pNodes[n] )
+        {
+            if ( n1 == -1 )
+                n1 = n;
+            else if ( n2 == -1 )
+            {
+                n2 = n;
+                break;
+            }
+        }
+    assert( n1 != -1 );
+    // check the situation when only one such node is detected
+    if ( n2 == -1 )
+    {
+        // save the node
+        pNode = pNodes[n1];
+        // clean the node
+        pNodes[n1] = NULL;
+        return pNode;
+    }
+  
+    // combines two nodes
+    pNode = Extra_CombineTwoNodes( dd, b1, pNodes[n1], pNodes[n2] );
+
+    // clean the old nodes
+    pNodes[n1] = pNode;
+    pNodes[n2] = NULL;
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube,
+    Extra_ImageNode_t * pNode1, Extra_ImageNode_t * pNode2 )
+{
+    Extra_ImageNode_t * pNode;
+    Extra_ImagePart_t * pPart;
+
+    // create a new partition
+    pPart = ALLOC( Extra_ImagePart_t, 1 );
+    memset( pPart, 0, sizeof(Extra_ImagePart_t) );
+    // create the function
+    pPart->bFunc = Cudd_bddAndAbstract( dd, pNode1->pPart->bFunc, pNode2->pPart->bFunc, bCube );
+    Cudd_Ref( pPart->bFunc );
+    // update the support the partition
+    pPart->bSupp = Cudd_bddAndAbstract( dd, pNode1->pPart->bSupp, pNode2->pPart->bSupp, bCube );
+    Cudd_Ref( pPart->bSupp );
+    // update the numbers
+    pPart->nSupp  = Extra_bddSuppSize( dd, pPart->bSupp );
+    pPart->nNodes = Cudd_DagSize( pPart->bFunc );
+    pPart->iPart = -1;
+/*
+PRB( dd, pNode1->pPart->bSupp );
+PRB( dd, pNode2->pPart->bSupp );
+PRB( dd, pPart->bSupp );
+*/
+    // create a new node
+    pNode = ALLOC( Extra_ImageNode_t, 1 );
+    memset( pNode, 0, sizeof(Extra_ImageNode_t) );
+    pNode->dd     = dd;
+    pNode->pPart  = pPart;
+    pNode->pNode1 = pNode1;
+    pNode->pNode2 = pNode2;
+    // compute the image
+    pNode->bImage = Cudd_bddAndAbstract( dd, pNode1->bImage, pNode2->bImage, bCube ); 
+    Cudd_Ref( pNode->bImage );
+    // save the cube
+    if ( bCube != b1 )
+    {
+        pNode->bCube = bCube;   Cudd_Ref( bCube );
+    }
+    return pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the best variable.]
+
+  Description [The variables is the best if the sum of squares of the
+  BDD sizes of the partitions, in which it participates, is the minimum.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_FindBestVariable( DdManager * dd,
+    int nNodes, Extra_ImageNode_t ** pNodes, 
+    int nVars,  Extra_ImageVar_t ** pVars )
+{
+    DdNode * bTemp;
+    int iVarBest, v;
+    double CostBest, CostCur;
+
+    CostBest = 100000000000000;
+    iVarBest = -1;
+    for ( v = 0; v < nVars; v++ )
+        if ( pVars[v] )
+        {
+            CostCur = 0;
+            for ( bTemp = pVars[v]->bParts; bTemp != b1; bTemp = cuddT(bTemp) )
+                CostCur += pNodes[bTemp->index]->pPart->nNodes * 
+                           pNodes[bTemp->index]->pPart->nNodes;
+            if ( CostBest > CostCur )
+            {
+                CostBest = CostCur;
+                iVarBest = v;
+            }
+        }
+    return iVarBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes two smallest partions that have this var.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_FindBestPartitions( DdManager * dd, DdNode * bParts, 
+    int nNodes, Extra_ImageNode_t ** pNodes, 
+    int * piNode1, int * piNode2 )
+{
+    DdNode * bTemp;
+    int iPart1, iPart2;
+    int CostMin1, CostMin2, Cost;
+
+    // go through the partitions
+    iPart1 = iPart2 = -1;
+    CostMin1 = CostMin2 = 1000000;
+    for ( bTemp = bParts; bTemp != b1; bTemp = cuddT(bTemp) )
+    {
+        Cost = pNodes[bTemp->index]->pPart->nNodes;
+        if ( CostMin1 > Cost )
+        {
+            CostMin2 = CostMin1;    iPart2 = iPart1;
+            CostMin1 = Cost;        iPart1 = bTemp->index;
+        }
+        else if ( CostMin2 > Cost )
+        {
+            CostMin2 = Cost;        iPart2 = bTemp->index;
+        }
+    }
+
+    *piNode1 = iPart1;
+    *piNode2 = iPart2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the latch dependency matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_bddImagePrintLatchDependency( 
+    DdManager * dd, DdNode * bCare, // the care set
+    int nParts, DdNode ** pbParts,  // the partitions for image computation
+    int nVars, DdNode ** pbVars )   // the NS and parameter variables (not quantified!)
+{
+    int i;
+    DdNode * bVarsCs, * bVarsNs;
+
+    bVarsCs = Cudd_Support( dd, bCare );                       Cudd_Ref( bVarsCs );
+    bVarsNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars );  Cudd_Ref( bVarsNs );
+
+    printf( "The latch dependency matrix:\n" );
+    printf( "Partitions = %d   Variables: total = %d  non-quantifiable = %d\n",
+        nParts, dd->size, nVars );
+    printf( "     : " );
+    for ( i = 0; i < dd->size; i++ )
+        printf( "%d", i % 10 );
+    printf( "\n" );
+
+    for ( i = 0; i < nParts; i++ )
+        Extra_bddImagePrintLatchDependencyOne( dd, pbParts[i], bVarsCs, bVarsNs, i );
+    Extra_bddImagePrintLatchDependencyOne( dd, bCare, bVarsCs, bVarsNs, nParts );
+
+    Cudd_RecursiveDeref( dd, bVarsCs );
+    Cudd_RecursiveDeref( dd, bVarsNs );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints one row of the latch dependency matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_bddImagePrintLatchDependencyOne(
+    DdManager * dd, DdNode * bFunc,      // the function
+    DdNode * bVarsCs, DdNode * bVarsNs,  // the current/next state vars
+    int iPart )
+{
+    DdNode * bSupport;
+    int v;
+    bSupport = Cudd_Support( dd, bFunc );  Cudd_Ref( bSupport );
+    printf( " %3d : ", iPart );
+    for ( v = 0; v < dd->size; v++ )
+    {
+        if ( Cudd_bddLeq( dd, bSupport, dd->vars[v] ) )
+        {
+            if ( Cudd_bddLeq( dd, bVarsCs, dd->vars[v] ) )
+                printf( "c" );
+            else if ( Cudd_bddLeq( dd, bVarsNs, dd->vars[v] ) ) 
+                printf( "n" );
+            else
+                printf( "i" );
+        }
+        else
+            printf( "." );
+    }
+    printf( "\n" );
+    Cudd_RecursiveDeref( dd, bSupport );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the tree for quenstification scheduling.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_bddImagePrintTree( Extra_ImageTree_t * pTree )
+{
+    printf( "The quantification scheduling tree:\n" );
+    Extra_bddImagePrintTree_rec( pTree->pRoot, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the tree for quenstification scheduling.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int Offset )
+{
+    DdNode * Cube;
+    int i;
+
+    Cube = pNode->bCube;
+
+    if ( pNode->pNode1 == NULL )
+    {
+        printf( "<%d> ", pNode->pPart->iPart );
+        if ( Cube != NULL )
+        {
+            PRB( pNode->dd, Cube );
+        }
+        else
+            printf( "\n" );
+        return;
+    }
+
+    printf( "<*> " );
+    if ( Cube != NULL )
+    {
+        PRB( pNode->dd, Cube );
+    }
+    else
+        printf( "\n" );
+
+    for ( i = 0; i < Offset; i++ )
+        printf( "    " );
+    Extra_bddImagePrintTree_rec( pNode->pNode1, Offset + 1 );
+
+    for ( i = 0; i < Offset; i++ )
+        printf( "    " );
+    Extra_bddImagePrintTree_rec( pNode->pNode2, Offset + 1 );
+}
+
+
+
+
+
+struct Extra_ImageTree2_t_
+{
+    DdManager * dd;
+    DdNode *    bRel;
+    DdNode *    bCube;
+    DdNode *    bImage;
+};
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the monolithic image computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Extra_ImageTree2_t * Extra_bddImageStart2( 
+    DdManager * dd, DdNode * bCare,
+    int nParts, DdNode ** pbParts,
+    int nVars, DdNode ** pbVars, int fVerbose )
+{
+    Extra_ImageTree2_t * pTree;
+    DdNode * bCubeAll, * bCubeNot, * bTemp;
+    int i;
+
+    pTree = ALLOC( Extra_ImageTree2_t, 1 );
+    pTree->dd = dd;
+    pTree->bImage = NULL;
+
+    bCubeAll = Extra_bddComputeCube( dd, dd->vars, dd->size );      Cudd_Ref( bCubeAll );
+    bCubeNot = Extra_bddComputeCube( dd, pbVars,   nVars );         Cudd_Ref( bCubeNot );
+    pTree->bCube = Cudd_bddExistAbstract( dd, bCubeAll, bCubeNot ); Cudd_Ref( pTree->bCube );
+    Cudd_RecursiveDeref( dd, bCubeAll );
+    Cudd_RecursiveDeref( dd, bCubeNot );
+
+    // derive the monolithic relation
+    pTree->bRel = b1;   Cudd_Ref( pTree->bRel );
+    for ( i = 0; i < nParts; i++ )
+    {
+        pTree->bRel = Cudd_bddAnd( dd, bTemp = pTree->bRel, pbParts[i] ); Cudd_Ref( pTree->bRel );
+        Cudd_RecursiveDeref( dd, bTemp );
+    }
+    Extra_bddImageCompute2( pTree, bCare );
+    return pTree;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare )
+{
+    if ( pTree->bImage )
+        Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
+    pTree->bImage = Cudd_bddAndAbstract( pTree->dd, pTree->bRel, bCare, pTree->bCube ); 
+    Cudd_Ref( pTree->bImage );
+    return pTree->bImage;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree )
+{
+    if ( pTree->bRel )
+        Cudd_RecursiveDeref( pTree->dd, pTree->bRel );
+    if ( pTree->bCube )
+        Cudd_RecursiveDeref( pTree->dd, pTree->bCube );
+    if ( pTree->bImage )
+        Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
+    FREE( pTree );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the previously computed image.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Extra_bddImageRead2( Extra_ImageTree2_t * pTree )
+{
+    return pTree->bImage;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index e4790325..023a9841 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -961,6 +961,34 @@ void Extra_bddPermuteArray( DdManager * manager, DdNode ** bNodesIn, DdNode ** b
 }    /* end of Extra_bddPermuteArray */
 
 
+/**Function********************************************************************
+
+  Synopsis    [Computes the positive polarty cube composed of the first vars in the array.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars )
+{
+    DdNode * bRes;
+    DdNode * bTemp;
+    int i;
+
+    bRes = b1; Cudd_Ref( bRes );
+    for ( i = 0; i < nVars; i++ )
+    {
+        bRes = Cudd_bddAnd( dd, bTemp = bRes, bXVars[i] );  Cudd_Ref( bRes );
+        Cudd_RecursiveDeref( dd, bTemp );
+    }
+
+    Cudd_Deref( bRes );
+    return bRes;
+}
+
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */
 /*---------------------------------------------------------------------------*/
diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make
index ec8bca4d..c7c9be4e 100644
--- a/src/misc/extra/module.make
+++ b/src/misc/extra/module.make
@@ -1,5 +1,6 @@
 SRC +=    src/misc/extra/extraBddAuto.c \
     src/misc/extra/extraBddCas.c \
+    src/misc/extra/extraBddImage.c \
     src/misc/extra/extraBddKmap.c \
     src/misc/extra/extraBddMisc.c \
     src/misc/extra/extraBddSymm.c \
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 7104d3b3..a941f153 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -241,21 +241,23 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     if ( pNtk->pExcare )
     {
         Abc_Ntk_t * pTemp;
-        pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 );
-        p->pCare = Abc_NtkToDar( pTemp, 0 );
-        Abc_NtkDelete( pTemp );
-        p->vSuppsInv = Aig_ManSupportsInverse( p->pCare );
-    }
-//    if ( pPars->fVerbose )
-    {
-        if ( p->pCare != NULL )
-            printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) );
-//        else
-//            printf( "Performing optimization without constraints.\n" );
+        if ( Abc_NtkPiNum(pNtk->pExcare) != Abc_NtkCiNum(pNtk) )
+            printf( "The PI count of careset (%d) and logic network (%d) differ. Careset is not used.\n", 
+                Abc_NtkPiNum(pNtk->pExcare), Abc_NtkCiNum(pNtk) );
+        else
+        {
+            pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 );
+            p->pCare = Abc_NtkToDar( pTemp, 0 );
+            Abc_NtkDelete( pTemp );
+            p->vSuppsInv = Aig_ManSupportsInverse( p->pCare );
+        }
     }
+    if ( p->pCare != NULL )
+        printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) );
+    // prepare the BDC manager
     if ( !pPars->fResub )
     {
-        pDecPars->nVarsMax = nFaninMax;
+        pDecPars->nVarsMax = (nFaninMax < 3) ? 3 : nFaninMax;
         pDecPars->fVerbose = pPars->fVerbose;
         p->vTruth = Vec_IntAlloc( 0 );
         p->pManDec = Bdc_ManAlloc( pDecPars );