Version abc90118

6 files changed, 673 insertions, 114 deletions

diff --git a/src/aig/cgt/cgt.h b/src/aig/cgt/cgt.h
index b9997d56..f8c1cc2e 100644
--- a/src/aig/cgt/cgt.h
+++ b/src/aig/cgt/cgt.h
@@ -52,8 +52,9 @@ struct Cgt_Par_t_
     int          nConfMax;       // the max number of conflicts at a node
     int          nVarsMin;       // the min number of variables to recycle the SAT solver
     int          nFlopsMin;      // the min number of flops needed to recycle the SAT solver
+    int          fAreaOnly;      // derive clock gating to minimize area
     int          fVerbose;       // verbosity flag
-
+    int          fVeryVerbose;   // verbosity flag
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cgt/cgtAig.c b/src/aig/cgt/cgtAig.c
index b30d3f16..d411c25a 100644
--- a/src/aig/cgt/cgtAig.c
+++ b/src/aig/cgt/cgtAig.c
@@ -67,7 +67,7 @@ void Cgt_ManDetectCandidates_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevel
 void Cgt_ManDetectCandidates( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevelMax, Vec_Ptr_t * vCands )
 {
     Vec_PtrClear( vCands );
-    if ( !Aig_ObjIsNode(Aig_ObjFanin0(pObj)) )
+    if ( !Aig_ObjIsNode(pObj) )
         return;
     Aig_ManIncrementTravId( pAig );
     Cgt_ManDetectCandidates_rec( pAig, pObj, nLevelMax, vCands );
@@ -136,6 +136,67 @@ void Cgt_ManDetectFanout( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nOdcMax, Vec_P
 
 /**Function*************************************************************
 
+  Synopsis    [Computes visited nodes in the topological order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cgt_ManCollectVisited_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vVisited )
+{
+    if ( Aig_ObjIsPi(pObj) )
+        return;
+    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(pAig, pObj);
+    assert( Aig_ObjIsNode(pObj) );
+    Cgt_ManCollectVisited_rec( pAig, Aig_ObjFanin0(pObj), vVisited );
+    Cgt_ManCollectVisited_rec( pAig, Aig_ObjFanin1(pObj), vVisited );
+    Vec_PtrPush( vVisited, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes visited nodes in the topological order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cgt_ManCollectVisited( Aig_Man_t * pAig, Vec_Ptr_t * vFanout, Vec_Ptr_t * vVisited )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Vec_PtrClear( vVisited );
+    Aig_ManIncrementTravId( pAig );
+    Vec_PtrForEachEntry( vFanout, pObj, i )
+        Cgt_ManCollectVisited_rec( pAig, pObj, vVisited );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Aig_Obj_t *  Aig_ObjChild0CopyVec( Vec_Ptr_t * vCopy, Aig_Obj_t * pObj )  
+{ return Aig_NotCond((Aig_Obj_t *)Vec_PtrEntry(vCopy, Aig_ObjFaninId0(pObj)), Aig_ObjFaninC0(pObj));  }
+static inline Aig_Obj_t *  Aig_ObjChild1CopyVec( Vec_Ptr_t * vCopy, Aig_Obj_t * pObj )  
+{ return Aig_NotCond((Aig_Obj_t *)Vec_PtrEntry(vCopy, Aig_ObjFaninId1(pObj)), Aig_ObjFaninC1(pObj));  }
+
+/**Function*************************************************************
+
   Synopsis    [Derives miter for clock-gating.]
 
   Description []
@@ -145,15 +206,46 @@ void Cgt_ManDetectFanout( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nOdcMax, Vec_P
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Obj_t * Cgt_ManConstructMiter( Cgt_Man_t * p, Aig_Man_t * pNew, Aig_Obj_t * pObjLo )
+Aig_Obj_t * Cgt_ManConstructCareCondition( Cgt_Man_t * p, Aig_Man_t * pNew, Aig_Obj_t * pObjLo, Vec_Ptr_t * vCopy0, Vec_Ptr_t * vCopy1 )
 {
-    Aig_Obj_t * pMiter, * pRoot;
+    Aig_Obj_t * pMiter, * pObj, * pTemp;
     int i;
     assert( Aig_ObjIsPi(pObjLo) );
-    pMiter = Aig_ManConst0( pNew );
+    // detect nodes and their cone
     Cgt_ManDetectFanout( p->pAig, pObjLo, p->pPars->nOdcMax, p->vFanout );
-    Vec_PtrForEachEntry( p->vFanout, pRoot, i )
-        pMiter = Aig_Or( pNew, pMiter, Aig_Exor(pNew, pRoot->pData, pRoot->pNext) );
+    Cgt_ManCollectVisited( p->pAig, p->vFanout, p->vVisited );
+    // add new variables if the observability condition depends on PI variables
+    Vec_PtrForEachEntry( p->vVisited, pObj, i )
+    {
+        assert( Aig_ObjIsNode(pObj) );
+        if ( Saig_ObjIsPi(p->pAig, Aig_ObjFanin0(pObj)) && Vec_PtrEntry(vCopy0, Aig_ObjFaninId0(pObj)) == NULL )
+        {
+            pTemp = Aig_ObjCreatePi( pNew );
+            Vec_PtrWriteEntry( vCopy0, Aig_ObjFaninId0(pObj), pTemp );
+            Vec_PtrWriteEntry( vCopy1, Aig_ObjFaninId0(pObj), pTemp );
+        }
+        if ( Saig_ObjIsPi(p->pAig, Aig_ObjFanin1(pObj)) && Vec_PtrEntry(vCopy0, Aig_ObjFaninId1(pObj)) == NULL )
+        {
+            pTemp = Aig_ObjCreatePi( pNew );
+            Vec_PtrWriteEntry( vCopy0, Aig_ObjFaninId1(pObj), pTemp );
+            Vec_PtrWriteEntry( vCopy1, Aig_ObjFaninId1(pObj), pTemp );
+        }
+    }
+    // construct AIGs for the nodes
+    Vec_PtrForEachEntry( p->vVisited, pObj, i )
+    {
+        pTemp = Aig_And( pNew, Aig_ObjChild0CopyVec(vCopy0, pObj), Aig_ObjChild1CopyVec(vCopy0, pObj) );
+        Vec_PtrWriteEntry( vCopy0, Aig_ObjId(pObj), pTemp );
+        pTemp = Aig_And( pNew, Aig_ObjChild0CopyVec(vCopy1, pObj), Aig_ObjChild1CopyVec(vCopy1, pObj) );
+        Vec_PtrWriteEntry( vCopy1, Aig_ObjId(pObj), pTemp );
+    }
+    // construct the care miter
+    pMiter = Aig_ManConst0( pNew );
+    Vec_PtrForEachEntry( p->vFanout, pObj, i )
+    {
+        pTemp = Aig_Exor( pNew, Vec_PtrEntry(vCopy0, Aig_ObjId(pObj)), Vec_PtrEntry(vCopy1, Aig_ObjId(pObj)) );
+        pMiter = Aig_Or( pNew, pMiter, pTemp );
+    }
     return pMiter;
 }
 
@@ -171,11 +263,12 @@ Aig_Obj_t * Cgt_ManConstructMiter( Cgt_Man_t * p, Aig_Man_t * pNew, Aig_Obj_t *
 Aig_Man_t * Cgt_ManDeriveAigForGating( Cgt_Man_t * p )
 {
     Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pCare, * pMiter;
+    Vec_Ptr_t * vCopy0, * vCopy1;
     int i;
     assert( Aig_ManRegNum(p->pAig) );
-    Aig_ManCleanNext( p->pAig );
     pNew = Aig_ManStart( Aig_ManObjNumMax(p->pAig) );
+    pNew->pName = Aig_UtilStrsav( "CG_miter" );
     // build the first frame
     Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew);
     Aig_ManForEachPi( p->pAig, pObj, i )
@@ -184,26 +277,128 @@ Aig_Man_t * Cgt_ManDeriveAigForGating( Cgt_Man_t * p )
         pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
 //    Saig_ManForEachPo( p->pAig, pObj, i )
 //        pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-    // build the second frame
-    Aig_ManConst1(p->pAig)->pNext = Aig_ManConst1(pNew);
-    Saig_ManForEachPi( p->pAig, pObj, i )
-        pObj->pNext = Aig_ObjCreatePi( pNew );
-    Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
-        pObjLo->pNext = Aig_ObjChild0Copy(pObjLi);
-    Aig_ManForEachNode( p->pAig, pObj, i )
-        if ( Aig_ObjLevel(pObj) <= p->pPars->nOdcMax )
-            pObj->pNext = Aig_And( pNew, Aig_ObjChild0Next(pObj), Aig_ObjChild1Next(pObj) );
-    // construct clock-gating miters for each register input
-    Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
-        pObjLi->pData = Aig_ObjCreatePo( pNew, Cgt_ManConstructMiter(p, pNew, pObjLo) );
-    Aig_ManCleanNext( p->pAig );
-    Aig_ManSetPioNumbers( p->pAig );
+    if ( p->pPars->nOdcMax > 0 )
+    {
+        // create storage for observability conditions
+        vCopy0 = Vec_PtrStart( Aig_ManObjNumMax(p->pAig) );
+        vCopy1 = Vec_PtrStart( Aig_ManObjNumMax(p->pAig) );
+        // initialize register outputs
+        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
+        {
+            Vec_PtrWriteEntry( vCopy0, Aig_ObjId(pObjLo), Aig_ObjChild0Copy(pObjLi) );
+            Vec_PtrWriteEntry( vCopy1, Aig_ObjId(pObjLo), Aig_ObjChild0Copy(pObjLi) );
+        }
+        // compute observability condition for each latch output
+        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
+        {
+            // set the constants
+            Vec_PtrWriteEntry( vCopy0, Aig_ObjId(pObjLo), Aig_ManConst0(pNew) );
+            Vec_PtrWriteEntry( vCopy1, Aig_ObjId(pObjLo), Aig_ManConst1(pNew) );
+            // compute condition
+            pCare = Cgt_ManConstructCareCondition( p, pNew, pObjLo, vCopy0, vCopy1 );
+            // restore the values
+            Vec_PtrWriteEntry( vCopy0, Aig_ObjId(pObjLo), Aig_ObjChild0Copy(pObjLi) );
+            Vec_PtrWriteEntry( vCopy1, Aig_ObjId(pObjLo), Aig_ObjChild0Copy(pObjLi) );
+            // compute the miter
+            pMiter = Aig_Exor( pNew, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) );
+            pMiter = Aig_And( pNew, pMiter, pCare );
+            pObjLi->pData = Aig_ObjCreatePo( pNew, pMiter );
+        }
+        Vec_PtrFree( vCopy0 );
+        Vec_PtrFree( vCopy1 );
+    }
+    else
+    {
+        // construct clock-gating miters for each register input
+        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
+        {
+            pMiter = Aig_Exor( pNew, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) );
+            pObjLi->pData = Aig_ObjCreatePo( pNew, pMiter );
+        }
+    }
     Aig_ManCleanup( pNew );
+    Aig_ManSetPioNumbers( pNew );
     return pNew;
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Adds relevant constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Cgt_ManConstructCare_rec( Aig_Man_t * pCare, Aig_Obj_t * pObj, Aig_Man_t * pNew )
+{
+    Aig_Obj_t * pObj0, * pObj1;
+    if ( Aig_ObjIsTravIdCurrent( pCare, pObj ) )
+        return pObj->pData;
+    Aig_ObjSetTravIdCurrent( pCare, pObj );
+    if ( Aig_ObjIsPi(pObj) )
+        return pObj->pData = NULL;
+    pObj0 = Cgt_ManConstructCare_rec( pCare, Aig_ObjFanin0(pObj), pNew );
+    if ( pObj0 == NULL )
+        return pObj->pData = NULL;
+    pObj1 = Cgt_ManConstructCare_rec( pCare, Aig_ObjFanin1(pObj), pNew );
+    if ( pObj1 == NULL )
+        return pObj->pData = NULL;
+    pObj0 = Aig_NotCond( pObj0, Aig_ObjFaninC0(pObj) );
+    pObj1 = Aig_NotCond( pObj1, Aig_ObjFaninC1(pObj) );
+    return pObj->pData = Aig_And( pNew, pObj0, pObj1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Builds constraints belonging to the given partition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cgt_ManConstructCare( Aig_Man_t * pNew, Aig_Man_t * pCare, Vec_Vec_t * vSuppsInv, Vec_Ptr_t * vLeaves )
+{
+    Vec_Int_t * vOuts;
+    Aig_Obj_t * pLeaf, * pPi, * pPo, * pObjAig;
+    int i, k, iOut;
+    // go through the PIs of the partition
+    // label the corresponding PIs of the care set
+    Aig_ManIncrementTravId( pCare );
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        pPi = Aig_ManPi( pCare, Aig_ObjPioNum(pLeaf) );
+        Aig_ObjSetTravIdCurrent( pCare, pPi );
+        pPi->pData = pLeaf->pData;
+    }
+    // construct the constraints
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        vOuts = Vec_VecEntry( vSuppsInv, Aig_ObjPioNum(pLeaf) );
+        Vec_IntForEachEntry( vOuts, iOut, k )
+        {
+            pPo = Aig_ManPo( pCare, iOut );
+            if ( Aig_ObjIsTravIdCurrent( pCare, pPo ) )
+                continue;
+            Aig_ObjSetTravIdCurrent( pCare, pPo );
+            if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(pCare) )
+                continue;
+            pObjAig = Cgt_ManConstructCare_rec( pCare, Aig_ObjFanin0(pPo), pNew );
+            if ( pObjAig == NULL )
+                continue;
+            pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
+            Aig_ObjCreatePo( pNew, pObjAig );
+        }
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates the AIG recursively.]
 
   Description []
@@ -213,15 +408,19 @@ Aig_Man_t * Cgt_ManDeriveAigForGating( Cgt_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Obj_t * Cgt_ManDupPartition_rec( Aig_Man_t * pNew, Aig_Man_t * pAig, Aig_Obj_t * pObj )
+Aig_Obj_t * Cgt_ManDupPartition_rec( Aig_Man_t * pNew, Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vLeaves )
 {
     if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
         return pObj->pData;
     Aig_ObjSetTravIdCurrent(pAig, pObj);
     if ( Aig_ObjIsPi(pObj) )
-        return pObj->pData = Aig_ObjCreatePi( pNew );
-    Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
-    Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin1(pObj) );
+    {
+        pObj->pData = Aig_ObjCreatePi( pNew );
+        Vec_PtrPush( vLeaves, pObj );
+        return pObj->pData;
+    }
+    Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin0(pObj), vLeaves );
+    Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin1(pObj), vLeaves );
     return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
 }
 
@@ -236,34 +435,80 @@ Aig_Obj_t * Cgt_ManDupPartition_rec( Aig_Man_t * pNew, Aig_Man_t * pAig, Aig_Obj
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Cgt_ManDupPartition( Aig_Man_t * pAig, int nVarsMin, int nFlopsMin, int iStart )
+Aig_Man_t * Cgt_ManDupPartition( Aig_Man_t * pFrame, int nVarsMin, int nFlopsMin, int iStart, Aig_Man_t * pCare, Vec_Vec_t * vSuppsInv, int * pnOutputs )
 {
+    Vec_Ptr_t * vRoots, * vLeaves, * vPos;
     Aig_Man_t * pNew;
     Aig_Obj_t * pObj;
     int i;
-    assert( Aig_ManRegNum(pAig) == 0 );
+    assert( Aig_ManRegNum(pFrame) == 0 );
+    vRoots = Vec_PtrAlloc( 100 );
+    vLeaves = Vec_PtrAlloc( 100 ); 
+    vPos = Vec_PtrAlloc( 100 );
     pNew = Aig_ManStart( nVarsMin );
-    Aig_ManIncrementTravId( pAig );
-    Aig_ManConst1(pAig)->pData = Aig_ManConst1(pNew);
-    Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
-    for ( i = iStart; i < iStart + nFlopsMin && i < Aig_ManPoNum(pAig); i++ )
+    pNew->pName = Aig_UtilStrsav( "partition" );
+    Aig_ManIncrementTravId( pFrame );
+    Aig_ManConst1(pFrame)->pData = Aig_ManConst1(pNew);
+    Aig_ObjSetTravIdCurrent( pFrame, Aig_ManConst1(pFrame) );
+    for ( i = iStart; i < iStart + nFlopsMin && i < Aig_ManPoNum(pFrame); i++ )
     {
-        pObj = Aig_ManPo( pAig, i );
-        Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
-        pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        pObj = Aig_ManPo( pFrame, i );
+        Cgt_ManDupPartition_rec( pNew, pFrame, Aig_ObjFanin0(pObj), vLeaves );
+        Vec_PtrPush( vRoots, Aig_ObjChild0Copy(pObj) );
+        Vec_PtrPush( vPos, pObj );
     }
-    for ( ; Aig_ManObjNum(pNew) < nVarsMin && i < Aig_ManPoNum(pAig); i++ )
+    for ( ; Aig_ManObjNum(pNew) < nVarsMin && i < Aig_ManPoNum(pFrame); i++ )
     {
-        pObj = Aig_ManPo( pAig, i );
-        Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
-        pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        pObj = Aig_ManPo( pFrame, i );
+        Cgt_ManDupPartition_rec( pNew, pFrame, Aig_ObjFanin0(pObj), vLeaves );
+        Vec_PtrPush( vRoots, Aig_ObjChild0Copy(pObj) );
+        Vec_PtrPush( vPos, pObj );
     }
-    assert( nFlopsMin >= Aig_ManPoNum(pAig) || Aig_ManPoNum(pNew) >= nFlopsMin );
+    assert( nFlopsMin >= Vec_PtrSize(vRoots) || Vec_PtrSize(vRoots) >= nFlopsMin );
+    // create constaints
+    if ( pCare )
+        Cgt_ManConstructCare( pNew, pCare, vSuppsInv, vLeaves );
+    // create POs
+    Vec_PtrForEachEntry( vPos, pObj, i )
+        pObj->pData = Aig_ObjCreatePo( pNew, Vec_PtrEntry(vRoots, i) );
+    if ( pnOutputs != NULL )
+        *pnOutputs = Vec_PtrSize( vPos );
+    Vec_PtrFree( vRoots );
+    Vec_PtrFree( vLeaves );
+    Vec_PtrFree( vPos );
     return pNew;
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Implements one clock-gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Cgt_ManBuildClockGate( Aig_Man_t * pNew, Vec_Ptr_t * vGates )
+{
+    Aig_Obj_t * pGate, * pTotal;
+    int i;
+    assert( Vec_PtrSize(vGates) > 0 );
+    pTotal = Aig_ManConst0(pNew);
+    Vec_PtrForEachEntry( vGates, pGate, i )
+    {
+        if ( Aig_Regular(pGate)->pNext )
+            pGate = Aig_NotCond( Aig_Regular(pGate)->pNext, Aig_IsComplement(pGate) );
+        else
+            pGate = Aig_NotCond( Aig_Regular(pGate)->pData, Aig_IsComplement(pGate) );
+        pTotal = Aig_Or( pNew, pTotal, pGate );
+    }
+    return pTotal;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Derives AIG after clock-gating.]
 
   Description [The array contains, for each flop, its gate if present.]
@@ -273,34 +518,74 @@ Aig_Man_t * Cgt_ManDupPartition( Aig_Man_t * pAig, int nVarsMin, int nFlopsMin,
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Cgt_ManDeriveGatedAig( Aig_Man_t * pAig, Vec_Ptr_t * vGates )
+Aig_Man_t * Cgt_ManDeriveGatedAig( Aig_Man_t * pAig, Vec_Vec_t * vGates, int fReduce, int * pnUsedNodes )
 {
     Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo, * pGate, * pGateNew;
-    int i;
+    Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo, * pGateNew;
+    Vec_Ptr_t * vOne;
+    int i, k;
+    Aig_ManCleanNext( pAig );
+    // label nodes
+    Vec_VecForEachEntry( vGates, pObj, i, k )
+    {
+        if ( Aig_IsComplement(pObj) )
+            Aig_Regular(pObj)->fMarkB = 1;
+        else
+            Aig_Regular(pObj)->fMarkA = 1;
+    }
+    // construct AIG
     assert( Aig_ManRegNum(pAig) );
     pNew = Aig_ManStart( Aig_ManObjNumMax(pAig) );
+    pNew->pName = Aig_UtilStrsav( pAig->pName );
+    pNew->pSpec = Aig_UtilStrsav( pAig->pSpec );
     Aig_ManConst1(pAig)->pData = Aig_ManConst1(pNew);
     Aig_ManForEachPi( pAig, pObj, i )
         pObj->pData = Aig_ObjCreatePi( pNew );
-    Aig_ManForEachNode( pAig, pObj, i )
-        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    if ( fReduce )
+    {
+        Aig_ManForEachNode( pAig, pObj, i )
+        {
+            assert( !(pObj->fMarkA && pObj->fMarkB) );
+            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+            if ( pObj->fMarkA )
+            {
+                pObj->pNext = pObj->pData;
+                pObj->pData = Aig_ManConst0(pNew);
+            }
+            else if ( pObj->fMarkB )
+            {
+                pObj->pNext = pObj->pData;
+                pObj->pData = Aig_ManConst1(pNew);
+            }
+        }
+    }
+    else
+    {
+        Aig_ManForEachNode( pAig, pObj, i )
+            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    }
+    if ( pnUsedNodes != NULL )
+        *pnUsedNodes = Aig_ManNodeNum(pNew);
     Saig_ManForEachPo( pAig, pObj, i )
         pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
     Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
     {
-        pGate = Vec_PtrEntry( vGates, i );
-        if ( pGate == NULL )
+        vOne = Vec_VecEntry( vGates, i );
+        if ( Vec_PtrSize(vOne) == 0 )
             pObjNew = Aig_ObjChild0Copy(pObjLi);
         else
         {
-            pGateNew = Aig_NotCond( Aig_Regular(pGate)->pData, Aig_IsComplement(pGate) );
+//            pGateNew = Aig_NotCond( Aig_Regular(pGate)->pData, Aig_IsComplement(pGate) );
+            pGateNew = Cgt_ManBuildClockGate( pNew, vOne );
             pObjNew = Aig_Mux( pNew, pGateNew, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) );
         }
         pObjLi->pData = Aig_ObjCreatePo( pNew, pObjNew );
     }
     Aig_ManCleanup( pNew );
     Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) );
+    // unlabel nodes
+    Aig_ManCleanMarkAB( pAig );
+    Aig_ManCleanNext( pAig );
     return pNew;
 }
 
diff --git a/src/aig/cgt/cgtCore.c b/src/aig/cgt/cgtCore.c
index a06820b4..f49cd46f 100644
--- a/src/aig/cgt/cgtCore.c
+++ b/src/aig/cgt/cgtCore.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "cgtInt.h"
+#include "bar.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -42,13 +43,14 @@
 void Cgt_SetDefaultParams( Cgt_Par_t * p )
 {
     memset( p, 0, sizeof(Cgt_Par_t) );
-    p->nLevelMax  =  1000;   // the max number of levels to look for clock-gates
+    p->nLevelMax  =    25;   // the max number of levels to look for clock-gates
     p->nCandMax   =  1000;   // the max number of candidates at each node
     p->nOdcMax    =     0;   // the max number of ODC levels to consider
-    p->nConfMax   =  1000;   // the max number of conflicts at a node
-    p->nVarsMin   =  5000;   // the min number of vars to recycle the SAT solver
-    p->nFlopsMin  =    25;   // the min number of flops to recycle the SAT solver
-    p->fVerbose   =     0;   // verbosity flag
+    p->nConfMax   =    10;   // the max number of conflicts at a node
+    p->nVarsMin   =  1000;   // the min number of vars to recycle the SAT solver
+    p->nFlopsMin  =     5;   // the min number of flops to recycle the SAT solver
+    p->fAreaOnly  =     0;   // derive clock-gating to minimize area
+    p->fVerbose   =     1;   // verbosity flag
 }
 
 /**Function*************************************************************
@@ -62,14 +64,14 @@ void Cgt_SetDefaultParams( Cgt_Par_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Cgt_SimulationFilter( Cgt_Man_t * p, Aig_Obj_t * pCandFrame, Aig_Obj_t * pMiterFrame )
+int Cgt_SimulationFilter( Cgt_Man_t * p, Aig_Obj_t * pCandPart, Aig_Obj_t * pMiterPart )
 {
     unsigned * pInfoCand, * pInfoMiter;
     int w, nWords = Aig_BitWordNum( p->nPatts );  
-    pInfoCand  = Vec_PtrEntry( p->vPatts, Aig_ObjId(Aig_Regular(pCandFrame)) );
-    pInfoMiter = Vec_PtrEntry( p->vPatts, Aig_ObjId(pMiterFrame) );
+    pInfoCand  = Vec_PtrEntry( p->vPatts, Aig_ObjId(Aig_Regular(pCandPart)) );
+    pInfoMiter = Vec_PtrEntry( p->vPatts, Aig_ObjId(pMiterPart) );
     // C => !M -- true   is the same as    C & M -- false
-    if ( !Aig_IsComplement(pCandFrame) )
+    if ( !Aig_IsComplement(pCandPart) )
     {
         for ( w = 0; w < nWords; w++ )
             if ( pInfoCand[w] & pInfoMiter[w] )
@@ -106,6 +108,7 @@ void Cgt_SimulationRecord( Cgt_Man_t * p )
     if ( p->nPatts == 32 * p->nPattWords )
     {
         Vec_PtrReallocSimInfo( p->vPatts );
+        Vec_PtrCleanSimInfo( p->vPatts, p->nPattWords, 2 * p->nPattWords );
         p->nPattWords *= 2;
     }
 }
@@ -121,15 +124,16 @@ void Cgt_SimulationRecord( Cgt_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Cgt_ClockGatingRangeCheck( Cgt_Man_t * p, int iStart )
+void Cgt_ClockGatingRangeCheck( Cgt_Man_t * p, int iStart, int nOutputs )
 {
     Vec_Ptr_t * vNodes = p->vFanout;
     Aig_Obj_t * pMiter, * pCand, * pMiterFrame, * pCandFrame, * pMiterPart, * pCandPart;
-    int i, k, RetValue;
+    int i, k, RetValue, nCalls;
     assert( Vec_VecSize(p->vGatesAll) == Aig_ManPoNum(p->pFrame) );
     // go through all the registers inputs of this range
-    for ( i = iStart; i < iStart + Aig_ManPoNum(p->pPart); i++ )
+    for ( i = iStart; i < iStart + nOutputs; i++ )
     {
+        nCalls = p->nCalls;
         pMiter = Saig_ManLi( p->pAig, i );
         Cgt_ManDetectCandidates( p->pAig, Aig_ObjFanin0(pMiter), p->pPars->nLevelMax, vNodes );
         // go through the candidates of this PO
@@ -153,6 +157,8 @@ void Cgt_ClockGatingRangeCheck( Cgt_Man_t * p, int iStart )
                 if ( RetValue == 0 )
                     Cgt_SimulationRecord( p );
             }
+            else
+                p->nCallsFiltered++;
             // try reverse polarity
             if ( Cgt_SimulationFilter( p, Aig_Not(pCandPart), pMiterPart ) )
             {
@@ -165,9 +171,18 @@ void Cgt_ClockGatingRangeCheck( Cgt_Man_t * p, int iStart )
                 if ( RetValue == 0 )
                     Cgt_SimulationRecord( p );
             }
+            else
+                p->nCallsFiltered++;
         }
+
+        if ( p->pPars->fVerbose )
+        {
+//            printf( "Flop %3d : Cand = %4d. Gate = %4d. SAT calls = %3d.\n", 
+//                i, Vec_PtrSize(vNodes), Vec_PtrSize(Vec_VecEntry(p->vGatesAll, i)), p->nCalls-nCalls );
+        }
+
     }
-}
+} 
 
 /**Function*************************************************************
 
@@ -182,16 +197,33 @@ void Cgt_ClockGatingRangeCheck( Cgt_Man_t * p, int iStart )
 ***********************************************************************/
 int Cgt_ClockGatingRange( Cgt_Man_t * p, int iStart )
 {
-    int iStop;
-    p->pPart = Cgt_ManDupPartition( p->pFrame, p->pPars->nVarsMin, p->pPars->nFlopsMin, iStart );
-    p->pCnf  = Cnf_DeriveSimple( p->pPart, Aig_ManPoNum(p->pPart) );
+    int nOutputs, iStop, clk, clkTotal = clock();
+    int nCallsUnsat    = p->nCallsUnsat;
+    int nCallsSat      = p->nCallsSat;
+    int nCallsUndec    = p->nCallsUndec;
+    int nCallsFiltered = p->nCallsFiltered;
+clk = clock();
+    p->pPart = Cgt_ManDupPartition( p->pFrame, p->pPars->nVarsMin, p->pPars->nFlopsMin, iStart, p->pCare, p->vSuppsInv, &nOutputs );
+    p->pCnf  = Cnf_DeriveSimple( p->pPart, nOutputs );
     p->pSat  = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
     sat_solver_compress( p->pSat );
-    p->vPatts = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pPart), 16 );
+    p->vPatts = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pPart), p->nPattWords );
     Vec_PtrCleanSimInfo( p->vPatts, 0, p->nPattWords );
-    Cgt_ClockGatingRangeCheck( p, iStart );
-    iStop = iStart + Aig_ManPoNum(p->pPart);
+p->timePrepare += clock() - clk;
+    Cgt_ClockGatingRangeCheck( p, iStart, nOutputs );
+    iStop = iStart + nOutputs;
+    if ( p->pPars->fVeryVerbose )
+    {
+        printf( "%5d : D =%4d. C =%5d. Var =%6d. Pr =%5d. Cex =%5d. F =%4d. Saved =%6d. ",
+            iStart, iStop-iStart, Aig_ManPoNum(p->pPart)-nOutputs, p->pSat->size, 
+            p->nCallsUnsat-nCallsUnsat, 
+            p->nCallsSat  -nCallsSat, 
+            p->nCallsUndec-nCallsUndec,
+            p->nCallsFiltered-nCallsFiltered );
+        PRT( "Time", clock() - clkTotal );
+    }
     Cgt_ManClean( p );
+    p->nRecycles++;
     return iStop;
 }
 
@@ -208,18 +240,30 @@ int Cgt_ClockGatingRange( Cgt_Man_t * p, int iStart )
 ***********************************************************************/
 Vec_Vec_t * Cgt_ClockGatingCandidates( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars )
 {
-    Cgt_Par_t Pars;
+    Bar_Progress_t * pProgress = NULL;
+    Cgt_Par_t Pars; 
     Cgt_Man_t * p;
     Vec_Vec_t * vGatesAll;
-    int iStart;
+    int iStart, clk = clock(), clkTotal = clock();
+    // reset random numbers
+    Aig_ManRandom( 1 );
     if ( pPars == NULL )
         Cgt_SetDefaultParams( pPars = &Pars );    
     p = Cgt_ManCreate( pAig, pCare, pPars );
     p->pFrame = Cgt_ManDeriveAigForGating( p );
+p->timeAig += clock() - clk;
     assert( Aig_ManPoNum(p->pFrame) == Saig_ManRegNum(p->pAig) );
+    pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p->pFrame) );
     for ( iStart = 0; iStart < Aig_ManPoNum(p->pFrame); )
+    {
+        Bar_ProgressUpdate( pProgress, iStart, NULL );
         iStart = Cgt_ClockGatingRange( p, iStart );
+    }
+    Bar_ProgressStop( pProgress );
     vGatesAll = p->vGatesAll;
+    p->vGatesAll = NULL;
+p->timeTotal = clock() - clkTotal;
+    Cgt_ManStop( p );
     return vGatesAll;
 }
 
@@ -238,11 +282,29 @@ Aig_Man_t * Cgt_ClockGating( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pP
 {
     Aig_Man_t * pGated;
     Vec_Vec_t * vGatesAll;
-    Vec_Ptr_t * vGates;
+    Vec_Vec_t * vGates;
+    int nNodesUsed, clk = clock();
     vGatesAll = Cgt_ClockGatingCandidates( pAig, pCare, pPars );
-    vGates = Cgt_ManDecideSimple( pAig, vGatesAll );
-    pGated = Cgt_ManDeriveGatedAig( pAig, vGates );
-    Vec_PtrFree( vGates );
+    if ( pPars->fAreaOnly )
+        vGates = Cgt_ManDecideArea( pAig, vGatesAll, pPars->nOdcMax, pPars->fVerbose );
+    else
+        vGates = Cgt_ManDecideSimple( pAig, vGatesAll, pPars->nOdcMax, pPars->fVerbose );
+    if ( pPars->fVerbose )
+    {
+//        printf( "Before CG: " );
+//        Aig_ManPrintStats( pAig );
+    }
+    pGated = Cgt_ManDeriveGatedAig( pAig, vGates, pPars->fAreaOnly, &nNodesUsed );
+    if ( pPars->fVerbose )
+    {
+//        printf( "After  CG: " );
+//        Aig_ManPrintStats( pGated );
+        printf( "Nodes: Before CG = %6d. After CG = %6d. (%6.2f %%).  Total after CG = %6d.\n", 
+            Aig_ManNodeNum(pAig), nNodesUsed, 
+            100.0*nNodesUsed/Aig_ManNodeNum(pAig), 
+            Aig_ManNodeNum(pGated) );
+    }
+    Vec_VecFree( vGates );
     Vec_VecFree( vGatesAll );
     return pGated;
 }
diff --git a/src/aig/cgt/cgtDecide.c b/src/aig/cgt/cgtDecide.c
index 8f57bd4a..0fb2a681 100644
--- a/src/aig/cgt/cgtDecide.c
+++ b/src/aig/cgt/cgtDecide.c
@@ -25,8 +25,11 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern int Ssw_SmlCountXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand );
 extern int Ssw_SmlCheckXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand );
+extern int Ssw_SmlCountXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand );
+extern int Ssw_SmlCountEqual( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo );
+extern int Ssw_SmlNodeCountOnesReal( Ssw_Sml_t * p, Aig_Obj_t * pObj );
+extern int Ssw_SmlNodeCountOnesRealVec( Ssw_Sml_t * p, Vec_Ptr_t * vObjs );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -34,7 +37,7 @@ extern int Ssw_SmlCheckXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Ob
 
 /**Function*************************************************************
 
-  Synopsis    [Chooses what clock-gate to use for each register.]
+  Synopsis    [Collects POs in the transitive fanout.]
 
   Description []
                
@@ -43,11 +46,127 @@ extern int Ssw_SmlCheckXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Ob
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Cgt_ManDecide( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll )
+void Cgt_ManCollectFanoutPos_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vFanout )
+{
+    Aig_Obj_t * pFanout;
+    int f, iFanout;
+    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(pAig, pObj);
+    if ( Aig_ObjIsPo(pObj) )
+    {
+        Vec_PtrPush( vFanout, pObj );
+        return;
+    }
+    Aig_ObjForEachFanout( pAig, pObj, pFanout, iFanout, f )
+        Cgt_ManCollectFanoutPos_rec( pAig, pFanout, vFanout );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects POs in the transitive fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cgt_ManCollectFanoutPos( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vFanout )
+{
+    Vec_PtrClear( vFanout );
+    Aig_ManIncrementTravId( pAig );
+    Cgt_ManCollectFanoutPos_rec( pAig, pObj, vFanout );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if all PO fanouts can be gated by this node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cgt_ManCheckGateComplete( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, Aig_Obj_t * pGate, Vec_Ptr_t * vFanout )
 {
     Vec_Ptr_t * vGates;
-    vGates = Vec_PtrStart( Saig_ManRegNum(pAig) );
-    return vGates;
+    Aig_Obj_t * pObj;
+    int i;
+    Vec_PtrForEachEntry( vFanout, pObj, i )
+    {
+        if ( Saig_ObjIsPo(pAig, pObj) )
+            return 0;
+        vGates = Vec_VecEntry( vGatesAll, Aig_ObjPioNum(pObj) - Saig_ManPoNum(pAig) );
+        if ( Vec_PtrFind( vGates, pGate ) == -1 )
+            return 0;            
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the set of complete clock gates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Cgt_ManCompleteGates( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, int nOdcMax, int fVerbose )
+{
+    Vec_Ptr_t * vFanout, * vGatesFull;
+    Aig_Obj_t * pGate, * pGateR;
+    int i, k;
+    vFanout    = Vec_PtrAlloc( 100 );
+    vGatesFull = Vec_PtrAlloc( 100 );
+    Vec_VecForEachEntry( vGatesAll, pGate, i, k )
+    {
+        pGateR = Aig_Regular(pGate);
+        if ( pGateR->fMarkA )
+            continue;
+        pGateR->fMarkA = 1;
+        Cgt_ManCollectFanoutPos( pAig, pGateR, vFanout );
+        if ( Cgt_ManCheckGateComplete( pAig, vGatesAll, pGate, vFanout ) )
+            Vec_PtrPush( vGatesFull, pGate );
+    }
+    Vec_PtrFree( vFanout );
+    Vec_VecForEachEntry( vGatesAll, pGate, i, k )
+        Aig_Regular(pGate)->fMarkA = 0;
+    return vGatesFull;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Calculates coverage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Cgt_ManComputeCoverage( Aig_Man_t * pAig, Vec_Vec_t * vGates )
+{
+    int nFrames = 32;
+    int nWords  =  1;
+    Ssw_Sml_t * pSml;
+    Vec_Ptr_t * vOne;
+    int i, nTransTotal = 0, nTransSaved = 0;
+    pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
+    Vec_VecForEachLevel( vGates, vOne, i )
+    {
+        nTransSaved += Ssw_SmlNodeCountOnesRealVec( pSml, vOne );
+        nTransTotal += 32 * nFrames * nWords;
+    }
+    Ssw_SmlStop( pSml );
+    return (float)100.0*nTransSaved/nTransTotal;
 }
 
 /**Function*************************************************************
@@ -62,14 +181,18 @@ Vec_Ptr_t * Cgt_ManDecide( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll )
+Vec_Vec_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, int nOdcMax, int fVerbose )
 {
+    int nFrames = 32;
+    int nWords  =  1;
     Ssw_Sml_t * pSml;
-    Vec_Ptr_t * vGates, * vCands;
+    Vec_Vec_t * vGates;
+    Vec_Ptr_t * vCands;
     Aig_Obj_t * pObjLi, * pObjLo, * pCand, * pCandBest;
-    int i, k, nHitsCur, nHitsMax;
-    vGates = Vec_PtrStart( Saig_ManRegNum(pAig) );
-    pSml = Ssw_SmlSimulateSeq( pAig, 0, 32, 1 );
+    int i, k, nHitsCur, nHitsMax, Counter = 0, clk = clock();
+    int nTransTotal = 0, nTransSaved = 0;
+    vGates = Vec_VecStart( Saig_ManRegNum(pAig) );
+    pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
     Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
     {
         nHitsMax = 0;
@@ -78,10 +201,10 @@ Vec_Ptr_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll )
         Vec_PtrForEachEntry( vCands, pCand, k )
         {
             // check if this is indeed a clock-gate
-            if ( !Ssw_SmlCheckXorImplication( pSml, pObjLi, pObjLo, pCand ) )
+            if ( nOdcMax == 0 && !Ssw_SmlCheckXorImplication( pSml, pObjLi, pObjLo, pCand ) )
                 printf( "Clock gate candidate is invalid!\n" );
             // find its characteristic number
-            nHitsCur = Ssw_SmlCountXorImplication( pSml, pObjLi, pObjLo, pCand );
+            nHitsCur = Ssw_SmlNodeCountOnesReal( pSml, pCand );
             if ( nHitsMax < nHitsCur )
             {
                 nHitsMax = nHitsCur;
@@ -89,9 +212,80 @@ Vec_Ptr_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll )
             }
         }
         if ( pCandBest != NULL )
-            Vec_PtrWriteEntry( vGates, i, pCandBest );
+        {
+            Vec_VecPush( vGates, i, pCandBest );
+            Counter++;
+            nTransSaved += nHitsMax;
+        }
+        nTransTotal += 32 * nFrames * nWords;
     }
     Ssw_SmlStop( pSml );
+    if ( fVerbose )
+    {
+        printf( "Gating signals = %6d. Gated flops = %6d. (Total flops = %6d.)\n", 
+            Vec_VecSizeSize(vGatesAll), Counter, Saig_ManRegNum(pAig) );
+//        printf( "Gated transitions = %5.2f %%. (%5.2f %%.) ", 
+//            100.0*nTransSaved/nTransTotal, Cgt_ManComputeCoverage(pAig, vGates) );
+        printf( "Gated transitions = %5.2f %%. ", Cgt_ManComputeCoverage(pAig, vGates) );
+        PRT( "Time", clock() - clk );
+    }
+/*
+    {
+        Vec_Ptr_t * vCompletes;
+        vCompletes = Cgt_ManCompleteGates( pAig, vGatesAll, nOdcMax, fVerbose );
+        printf( "Complete gates = %d. \n", Vec_PtrSize(vCompletes) );
+        Vec_PtrFree( vCompletes );
+    }
+*/
+    return vGates;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the set of complete clock gates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Cgt_ManDecideArea( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, int nOdcMax, int fVerbose )
+{
+    Vec_Vec_t * vGates;
+    Vec_Ptr_t * vCompletes, * vOne;
+    Aig_Obj_t * pGate;
+    int i, k, Counter = 0, clk = clock();
+    // derive and label complete gates
+    vCompletes = Cgt_ManCompleteGates( pAig, vGatesAll, nOdcMax, fVerbose );
+    // label complete gates
+    Vec_PtrForEachEntry( vCompletes, pGate, i )
+        Aig_Regular(pGate)->fMarkA = 1;
+    // select only complete gates
+    vGates = Vec_VecStart( Saig_ManRegNum(pAig) );
+    Vec_VecForEachEntry( vGatesAll, pGate, i, k )
+        if ( Aig_Regular(pGate)->fMarkA )
+            Vec_VecPush( vGates, i, pGate );
+    // unlabel complete gates
+    Vec_PtrForEachEntry( vCompletes, pGate, i )
+        Aig_Regular(pGate)->fMarkA = 0;
+    // count the number of gated flops
+    Vec_VecForEachLevel( vGates, vOne, i )
+    {
+        Counter += (int)(Vec_PtrSize(vOne) > 0);
+//        printf( "%d ", Vec_PtrSize(vOne) );
+    }
+//    printf( "\n" );
+    if ( fVerbose )
+    {
+        printf( "Gating signals = %6d. Gated flops = %6d. (Total flops = %6d.)\n", 
+            Vec_VecSizeSize(vGatesAll), Counter, Saig_ManRegNum(pAig) );
+        printf( "Complete gates = %6d. Gated transitions = %5.2f %%. ", 
+            Vec_PtrSize(vCompletes), Cgt_ManComputeCoverage(pAig, vGates) );
+        PRT( "Time", clock() - clk );
+    }
+    Vec_PtrFree( vCompletes );
     return vGates;
 }
 
diff --git a/src/aig/cgt/cgtInt.h b/src/aig/cgt/cgtInt.h
index 7b4b6e63..23d851f3 100644
--- a/src/aig/cgt/cgtInt.h
+++ b/src/aig/cgt/cgtInt.h
@@ -48,12 +48,16 @@ struct Cgt_Man_t_
     // user's data
     Cgt_Par_t *  pPars;          // user's parameters
     Aig_Man_t *  pAig;           // user's AIG manager
-    Aig_Man_t *  pCare;          // user's constraints
+    // user's constraints
+    Aig_Man_t *  pCare;          // constraint cones
+    Vec_Vec_t *  vSuppsInv;      // inverse support of the constraints
+    // result of clock-gating
     Vec_Vec_t *  vGatesAll;      // the computed clock-gates
     Vec_Ptr_t *  vGates;         // the selected clock-gates
     // internal data
     Aig_Man_t *  pFrame;         // clock gate AIG manager
     Vec_Ptr_t *  vFanout;        // temporary storage for fanouts
+    Vec_Ptr_t *  vVisited;       // temporary storage for visited nodes
     // SAT solving
     Aig_Man_t *  pPart;          // partition
     Cnf_Dat_t *  pCnf;           // CNF of the partition
@@ -62,14 +66,21 @@ struct Cgt_Man_t_
     int          nPatts;         // the number of patterns accumulated
     int          nPattWords;     // the number of pattern words
     // statistics
+    int          nRecycles;      // recycles 
     int          nCalls;         // total calls
     int          nCallsSat;      // satisfiable calls
     int          nCallsUnsat;    // unsatisfiable calls  
     int          nCallsUndec;    // undecided calls
+    int          nCallsFiltered; // filtered out calls
+    int          timeAig;        // constructing AIG
+    int          timePrepare;    // partitioning and SAT solving
     int          timeSat;        // total runtime
     int          timeSatSat;     // satisfiable runtime 
     int          timeSatUnsat;   // unsatisfiable runtime 
     int          timeSatUndec;   // undecided runtime
+    int          timeDecision;   // making decision about what gates to use
+    int          timeOther;      // other runtime
+    int          timeTotal;      // total runtime
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -83,11 +94,11 @@ struct Cgt_Man_t_
 /*=== cgtAig.c ==========================================================*/
 extern void             Cgt_ManDetectCandidates( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevelMax, Vec_Ptr_t * vCands );
 extern Aig_Man_t *      Cgt_ManDeriveAigForGating( Cgt_Man_t * p );
-extern Aig_Man_t *      Cgt_ManDupPartition( Aig_Man_t * pAig, int nVarsMin, int nFlopsMin, int iStart );
-extern Aig_Man_t *      Cgt_ManDeriveGatedAig( Aig_Man_t * pAig, Vec_Ptr_t * vGates );
+extern Aig_Man_t *      Cgt_ManDupPartition( Aig_Man_t * pAig, int nVarsMin, int nFlopsMin, int iStart, Aig_Man_t * pCare, Vec_Vec_t * vSuppsInv, int * pnOutputs );
+extern Aig_Man_t *      Cgt_ManDeriveGatedAig( Aig_Man_t * pAig, Vec_Vec_t * vGates, int fReduce, int * pnUsedNodes );
 /*=== cgtDecide.c ==========================================================*/
-extern Vec_Ptr_t *      Cgt_ManDecide( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll );
-extern Vec_Ptr_t *      Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll );
+extern Vec_Vec_t *      Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, int nOdcMax, int fVerbose );
+extern Vec_Vec_t *      Cgt_ManDecideArea( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, int nOdcMax, int fVerbose );
 /*=== cgtMan.c ==========================================================*/
 extern Cgt_Man_t *      Cgt_ManCreate( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars );
 extern void             Cgt_ManClean( Cgt_Man_t * p );
diff --git a/src/aig/cgt/cgtMan.c b/src/aig/cgt/cgtMan.c
index 9615d2e6..a3385228 100644
--- a/src/aig/cgt/cgtMan.c
+++ b/src/aig/cgt/cgtMan.c
@@ -53,7 +53,19 @@ Cgt_Man_t * Cgt_ManCreate( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPar
     p->pAig       = pAig;
     p->vGatesAll  = Vec_VecStart( Saig_ManRegNum(pAig) );
     p->vFanout    = Vec_PtrAlloc( 1000 );
+    p->vVisited   = Vec_PtrAlloc( 1000 );
     p->nPattWords = 16;
+    if ( pCare == NULL )
+        return p;
+    // check out the constraints
+    if ( Aig_ManPiNum(pCare) != Aig_ManPiNum(pAig) )
+    {
+        printf( "The PI count of care (%d) and AIG (%d) differ. Careset is not used.\n", 
+            Aig_ManPiNum(pCare), Aig_ManPiNum(pAig) );
+        return p;
+    }
+    p->pCare = pCare;
+    p->vSuppsInv = (Vec_Vec_t *)Aig_ManSupportsInverse( p->pCare );
     return p;
 }
 
@@ -106,27 +118,16 @@ void Cgt_ManClean( Cgt_Man_t * p )
 ***********************************************************************/
 void Cgt_ManPrintStats( Cgt_Man_t * p )
 {
+    printf( "Params: LevMax = %d. CandMax = %d. OdcMax = %d. ConfMax = %d. VarMin = %d. FlopMin = %d.\n", 
+        p->pPars->nLevelMax, p->pPars->nCandMax, p->pPars->nOdcMax, 
+        p->pPars->nConfMax, p->pPars->nVarsMin, p->pPars->nFlopsMin );
+    printf( "SAT   : Calls = %d. Unsat = %d. Sat = %d. Fails = %d.  Recycles = %d.  ", 
+        p->nCalls, p->nCallsUnsat, p->nCallsSat, p->nCallsUndec, p->nRecycles );
+    PRT( "Time", p->timeTotal );
 /*
-    double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20);
-
-    printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f Mb.\n", 
-        p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory );
-    printf( "AIG       : PI = %d. PO = %d. Latch = %d. Node = %d.  Ave SAT vars = %d.\n", 
-        Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), 
-        0/p->pPars->nIters );
-    printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Lits proved = %d.\n", 
-        p->nSatProof, p->nSatCallsSat, p->nSatFailsReal, Cgt_ManCountEquivs(p) );
-    printf( "SAT solver: Vars max = %d. Calls max = %d. Recycles = %d. Sim rounds = %d.\n", 
-        p->nVarsMax, p->nCallsMax, p->nRecyclesTotal, p->nSimRounds );
-    printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
-        p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), 
-        p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
-
-    p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeMarkCones-p->timeSimSat-p->timeSat;
-    PRTP( "BMC        ", p->timeBmc,       p->timeTotal );
-    PRTP( "Spec reduce", p->timeReduce,    p->timeTotal );
-    PRTP( "Mark cones ", p->timeMarkCones, p->timeTotal );
-    PRTP( "Sim SAT    ", p->timeSimSat,    p->timeTotal );
+    p->timeOther = p->timeTotal-p->timeAig-p->timePrepare-p->timeSat-p->timeDecision;
+    PRTP( "AIG        ", p->timeAig,       p->timeTotal );
+    PRTP( "Prepare    ", p->timePrepare,   p->timeTotal );
     PRTP( "SAT solving", p->timeSat,       p->timeTotal );
     PRTP( "  unsat    ", p->timeSatUnsat,  p->timeTotal );
     PRTP( "  sat      ", p->timeSatSat,    p->timeTotal );
@@ -155,8 +156,13 @@ void Cgt_ManStop( Cgt_Man_t * p )
         Aig_ManStop( p->pFrame );
     Cgt_ManClean( p );
     Vec_PtrFree( p->vFanout );
-    Vec_PtrFree( p->vGates );
-    Vec_VecFree( p->vGatesAll );
+    Vec_PtrFree( p->vVisited );
+    if ( p->vGates )
+        Vec_PtrFree( p->vGates );
+    if ( p->vGatesAll )
+        Vec_VecFree( p->vGatesAll );
+    if ( p->vSuppsInv )
+        Vec_VecFree( p->vSuppsInv );
     free( p );
 }