Major restructuring of the code.

8 files changed, 1712 insertions, 0 deletions

diff --git a/src/opt/cgt/cgt.h b/src/opt/cgt/cgt.h
new file mode 100644
index 00000000..73edbfc3
--- /dev/null
+++ b/src/opt/cgt/cgt.h
@@ -0,0 +1,86 @@
+/**CFile****************************************************************
+
+  FileName    [cgt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Clock gating package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cgt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__aig__cgt__cgt_h
+#define ABC__aig__cgt__cgt_h
+
+
+/* 
+    The algorithm implemented in this package is based on the paper:
+    A. Hurst. "Automatic synthesis of clock gating logic with controlled 
+    netlist perturbation", DAC 2008.
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Cgt_Par_t_ Cgt_Par_t;
+struct Cgt_Par_t_
+{
+    int          nLevelMax;      // the max number of levels to look for clock-gates
+    int          nCandMax;       // the max number of candidates at each node
+    int          nOdcMax;        // the max number of ODC levels to consider
+    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
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== cgtCore.c ==========================================================*/
+extern void            Cgt_SetDefaultParams( Cgt_Par_t * p );
+extern Vec_Vec_t *     Cgt_ClockGatingCandidates( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars );
+extern Aig_Man_t *     Cgt_ClockGating( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars );
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/cgt/cgtAig.c b/src/opt/cgt/cgtAig.c
new file mode 100644
index 00000000..757ebb85
--- /dev/null
+++ b/src/opt/cgt/cgtAig.c
@@ -0,0 +1,601 @@
+/**CFile****************************************************************
+
+  FileName    [cgtAig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Clock gating package.]
+
+  Synopsis    [Creates AIG to compute clock-gating.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cgtAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cgtInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes transitive fanout cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cgt_ManDetectCandidates_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevelMax, Vec_Ptr_t * vCands )
+{
+    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(pAig, pObj);
+    if ( Aig_ObjIsNode(pObj) )
+    {
+        Cgt_ManDetectCandidates_rec( pAig, Aig_ObjFanin0(pObj), nLevelMax, vCands );
+        Cgt_ManDetectCandidates_rec( pAig, Aig_ObjFanin1(pObj), nLevelMax, vCands );
+    }
+    if ( Aig_ObjLevel(pObj) <= nLevelMax )
+        Vec_PtrPush( vCands, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes transitive fanout cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cgt_ManDetectCandidates( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevelMax, Vec_Ptr_t * vCands )
+{
+    Vec_PtrClear( vCands );
+    if ( !Aig_ObjIsNode(pObj) )
+        return;
+    Aig_ManIncrementTravId( pAig );
+    Cgt_ManDetectCandidates_rec( pAig, pObj, nLevelMax, vCands );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes transitive fanout cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cgt_ManDetectFanout_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nOdcMax, Vec_Ptr_t * vFanout )
+{
+    Aig_Obj_t * pFanout;
+    int f, iFanout;
+    if ( Aig_ObjIsPo(pObj) || Aig_ObjLevel(pObj) > nOdcMax )
+        return;
+    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(pAig, pObj);
+    Vec_PtrPush( vFanout, pObj );
+    Aig_ObjForEachFanout( pAig, pObj, pFanout, iFanout, f )
+        Cgt_ManDetectFanout_rec( pAig, pFanout, nOdcMax, vFanout );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes transitive fanout cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cgt_ManDetectFanout( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nOdcMax, Vec_Ptr_t * vFanout )
+{
+    Aig_Obj_t * pFanout;
+    int i, k, f, iFanout;
+    // collect visited nodes
+    Vec_PtrClear( vFanout );
+    Aig_ManIncrementTravId( pAig );
+    Cgt_ManDetectFanout_rec( pAig, pObj, nOdcMax, vFanout );
+    // remove those nodes whose fanout is included
+    k = 0;
+    Vec_PtrForEachEntry( Aig_Obj_t *, vFanout, pObj, i )
+    {
+        // go through the fanouts of this node
+        Aig_ObjForEachFanout( pAig, pObj, pFanout, iFanout, f )
+            if ( !Aig_ObjIsTravIdCurrent(pAig, pFanout) )
+                break;
+        if ( f == Aig_ObjRefs(pObj) ) // all fanouts are included
+            continue;
+        Vec_PtrWriteEntry( vFanout, k++, pObj );
+    }
+    Vec_PtrShrink( vFanout, k );
+    Vec_PtrSort( vFanout, (int (*)(void))Aig_ObjCompareIdIncrease );
+    assert( Vec_PtrSize(vFanout) > 0 );
+}
+
+/**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( Aig_Obj_t *, 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 []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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, * pObj, * pTemp;
+    int i;
+    assert( Aig_ObjIsPi(pObjLo) );
+    // detect nodes and their cone
+    Cgt_ManDetectFanout( p->pAig, pObjLo, p->pPars->nOdcMax, p->vFanout );
+    Cgt_ManCollectVisited( p->pAig, p->vFanout, p->vVisited );
+    // add new variables if the observability condition depends on PI variables
+    Vec_PtrForEachEntry( Aig_Obj_t *, 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( Aig_Obj_t *, 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( Aig_Obj_t *, p->vFanout, pObj, i )
+    {
+        pTemp = Aig_Exor( pNew, (Aig_Obj_t *)Vec_PtrEntry(vCopy0, Aig_ObjId(pObj)), (Aig_Obj_t *)Vec_PtrEntry(vCopy1, Aig_ObjId(pObj)) );
+        pMiter = Aig_Or( pNew, pMiter, pTemp );
+    }
+    return pMiter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives AIG for clock-gating.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Cgt_ManDeriveAigForGating( Cgt_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pCare, * pMiter;
+    Vec_Ptr_t * vCopy0, * vCopy1;
+    int i;
+    assert( Aig_ManRegNum(p->pAig) );
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p->pAig) );
+    pNew->pName = Abc_UtilStrsav( "CG_miter" );
+    // build the first frame
+    Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p->pAig, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    Aig_ManForEachNode( p->pAig, pObj, i )
+        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) );
+    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, (Aig_Obj_t *)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, (Aig_Obj_t *)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 (Aig_Obj_t *)pObj->pData;
+    Aig_ObjSetTravIdCurrent( pCare, pObj );
+    if ( Aig_ObjIsPi(pObj) )
+        return (Aig_Obj_t *)(pObj->pData = NULL);
+    pObj0 = Cgt_ManConstructCare_rec( pCare, Aig_ObjFanin0(pObj), pNew );
+    if ( pObj0 == NULL )
+        return (Aig_Obj_t *)(pObj->pData = NULL);
+    pObj1 = Cgt_ManConstructCare_rec( pCare, Aig_ObjFanin1(pObj), pNew );
+    if ( pObj1 == NULL )
+        return (Aig_Obj_t *)(pObj->pData = NULL);
+    pObj0 = Aig_NotCond( pObj0, Aig_ObjFaninC0(pObj) );
+    pObj1 = Aig_NotCond( pObj1, Aig_ObjFaninC1(pObj) );
+    return (Aig_Obj_t *)(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( Aig_Obj_t *, vLeaves, pLeaf, i )
+    {
+        pPi = Aig_ManPi( pCare, Aig_ObjPioNum(pLeaf) );
+        Aig_ObjSetTravIdCurrent( pCare, pPi );
+        pPi->pData = pLeaf->pData;
+    }
+    // construct the constraints
+    Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, i )
+    {
+        vOuts = Vec_VecEntryInt( 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 []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 (Aig_Obj_t *)pObj->pData;
+    Aig_ObjSetTravIdCurrent(pAig, pObj);
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        pObj->pData = Aig_ObjCreatePi( pNew );
+        Vec_PtrPush( vLeaves, pObj );
+        return (Aig_Obj_t *)pObj->pData;
+    }
+    Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin0(pObj), vLeaves );
+    Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin1(pObj), vLeaves );
+    return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates register outputs starting from the given one.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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(pFrame) == 0 );
+    vRoots = Vec_PtrAlloc( 100 );
+    vLeaves = Vec_PtrAlloc( 100 ); 
+    vPos = Vec_PtrAlloc( 100 );
+    pNew = Aig_ManStart( nVarsMin );
+    pNew->pName = Abc_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( 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(pFrame); i++ )
+    {
+        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 >= Vec_PtrSize(vRoots) || Vec_PtrSize(vRoots) >= nFlopsMin );
+    // create constaints
+    if ( pCare )
+        Cgt_ManConstructCare( pNew, pCare, vSuppsInv, vLeaves );
+    // create POs
+    Vec_PtrForEachEntry( Aig_Obj_t *, vPos, pObj, i )
+        pObj->pData = (Aig_Obj_t *)Aig_ObjCreatePo( pNew, (Aig_Obj_t *)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( Aig_Obj_t *, vGates, pGate, i )
+    {
+        if ( Aig_Regular(pGate)->pNext )
+            pGate = Aig_NotCond( Aig_Regular(pGate)->pNext, Aig_IsComplement(pGate) );
+        else
+            pGate = Aig_NotCond( (Aig_Obj_t *)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.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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, * pGateNew;
+    Vec_Ptr_t * vOne;
+    int i, k;
+    Aig_ManCleanNext( pAig );
+    // label nodes
+    Vec_VecForEachEntry( Aig_Obj_t *, 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 = Abc_UtilStrsav( pAig->pName );
+    pNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    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 = (Aig_Obj_t *)pObj->pData;
+                pObj->pData = Aig_ManConst0(pNew);
+            }
+            else if ( pObj->fMarkB )
+            {
+                pObj->pNext = (Aig_Obj_t *)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 )
+    {
+        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 = Cgt_ManBuildClockGate( pNew, vOne );
+            pObjNew = Aig_Mux( pNew, pGateNew, (Aig_Obj_t *)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;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/cgt/cgtCore.c b/src/opt/cgt/cgtCore.c
new file mode 100644
index 00000000..958080c9
--- /dev/null
+++ b/src/opt/cgt/cgtCore.c
@@ -0,0 +1,321 @@
+/**CFile****************************************************************
+
+  FileName    [cgtCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Clock gating package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cgtCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cgtInt.h"
+#include "src/misc/bar/bar.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cgt_SetDefaultParams( Cgt_Par_t * p )
+{
+    memset( p, 0, sizeof(Cgt_Par_t) );
+    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   =    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*************************************************************
+
+  Synopsis    [Returns 1 if simulation does not filter out this candidate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cgt_SimulationFilter( Cgt_Man_t * p, Aig_Obj_t * pCandPart, Aig_Obj_t * pMiterPart )
+{
+    unsigned * pInfoCand, * pInfoMiter;
+    int w, nWords = Abc_BitWordNum( p->nPatts );  
+    pInfoCand  = (unsigned *)Vec_PtrEntry( p->vPatts, Aig_ObjId(Aig_Regular(pCandPart)) );
+    pInfoMiter = (unsigned *)Vec_PtrEntry( p->vPatts, Aig_ObjId(pMiterPart) );
+    // C => !M -- true   is the same as    C & M -- false
+    if ( !Aig_IsComplement(pCandPart) )
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( pInfoCand[w] & pInfoMiter[w] )
+                return 0;
+    }
+    else
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( ~pInfoCand[w] & pInfoMiter[w] )
+                return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Saves one simulation pattern.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cgt_SimulationRecord( Cgt_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManForEachObj( p->pPart, pObj, i )
+        if ( sat_solver_var_value( p->pSat, p->pCnf->pVarNums[i] ) )
+            Abc_InfoSetBit( (unsigned *)Vec_PtrEntry(p->vPatts, i), p->nPatts );
+    p->nPatts++;
+    if ( p->nPatts == 32 * p->nPattWords )
+    {
+        Vec_PtrReallocSimInfo( p->vPatts );
+        Vec_PtrCleanSimInfo( p->vPatts, p->nPattWords, 2 * p->nPattWords );
+        p->nPattWords *= 2;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs clock-gating for the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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, nCalls;
+    assert( Vec_VecSize(p->vGatesAll) == Aig_ManPoNum(p->pFrame) );
+    // go through all the registers inputs of this range
+    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
+        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pCand, k )
+        {
+            // get the corresponding nodes from the frames
+            pCandFrame  = (Aig_Obj_t *)pCand->pData;
+            pMiterFrame = (Aig_Obj_t *)pMiter->pData;
+            // get the corresponding nodes from the part
+            pCandPart   = (Aig_Obj_t *)pCandFrame->pData;
+            pMiterPart  = (Aig_Obj_t *)pMiterFrame->pData;
+            // try direct polarity
+            if ( Cgt_SimulationFilter( p, pCandPart, pMiterPart ) )
+            {
+                RetValue = Cgt_CheckImplication( p, pCandPart, pMiterPart );
+                if ( RetValue == 1 )
+                {
+                    Vec_VecPush( p->vGatesAll, i, pCand );
+                    continue;
+                }
+                if ( RetValue == 0 )
+                    Cgt_SimulationRecord( p );
+            }
+            else
+                p->nCallsFiltered++;
+            // try reverse polarity
+            if ( Cgt_SimulationFilter( p, Aig_Not(pCandPart), pMiterPart ) )
+            {
+                RetValue = Cgt_CheckImplication( p, Aig_Not(pCandPart), pMiterPart );
+                if ( RetValue == 1 )
+                {
+                    Vec_VecPush( p->vGatesAll, i, Aig_Not(pCand) );
+                    continue;
+                }
+                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*************************************************************
+
+  Synopsis    [Performs clock-gating for the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cgt_ClockGatingRange( Cgt_Man_t * p, int iStart )
+{
+    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  = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
+    sat_solver_compress( p->pSat );
+    p->vPatts = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pPart), p->nPattWords );
+    Vec_PtrCleanSimInfo( p->vPatts, 0, p->nPattWords );
+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 );
+        ABC_PRT( "Time", clock() - clkTotal );
+    }
+    Cgt_ManClean( p );
+    p->nRecycles++;
+    return iStop;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs clock-gating for the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Cgt_ClockGatingCandidates( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars )
+{
+    Bar_Progress_t * pProgress = NULL;
+    Cgt_Par_t Pars; 
+    Cgt_Man_t * p;
+    Vec_Vec_t * vGatesAll;
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs clock-gating for the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Cgt_ClockGating( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars )
+{
+    Aig_Man_t * pGated;
+    Vec_Vec_t * vGatesAll;
+    Vec_Vec_t * vGates;
+    int nNodesUsed, clk = clock();
+    vGatesAll = Cgt_ClockGatingCandidates( pAig, pCare, pPars );
+    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;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/cgt/cgtDecide.c b/src/opt/cgt/cgtDecide.c
new file mode 100644
index 00000000..293bde85
--- /dev/null
+++ b/src/opt/cgt/cgtDecide.c
@@ -0,0 +1,301 @@
+/**CFile****************************************************************
+
+  FileName    [cgtMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Clock gating package.]
+
+  Synopsis    [Decide what gate to use for what flop.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cgtMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cgtInt.h"
+#include "src/proof/ssw/sswInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+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                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Collects POs in the transitive fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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;
+    Aig_Obj_t * pObj;
+    int i;
+    Vec_PtrForEachEntry( Aig_Obj_t *, 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( Aig_Obj_t *, 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( Aig_Obj_t *, 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*************************************************************
+
+  Synopsis    [Chooses what clock-gate to use for this register.]
+
+  Description [Currently uses the naive approach: For each register, 
+  choose the clock gate, which covers most of the transitions.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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_Vec_t * vGates;
+    Vec_Ptr_t * vCands;
+    Aig_Obj_t * pObjLi, * pObjLo, * pCand, * pCandBest;
+    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;
+        pCandBest = NULL;
+        vCands = Vec_VecEntry( vGatesAll, i );
+        Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pCand, k )
+        {
+            // check if this is indeed a clock-gate
+            if ( nOdcMax == 0 && !Ssw_SmlCheckXorImplication( pSml, pObjLi, pObjLo, pCand ) )
+                printf( "Clock gate candidate is invalid!\n" );
+            // find its characteristic number
+            nHitsCur = Ssw_SmlNodeCountOnesReal( pSml, pCand );
+            if ( nHitsMax < nHitsCur )
+            {
+                nHitsMax = nHitsCur;
+                pCandBest = pCand;
+            }
+        }
+        if ( pCandBest != NULL )
+        {
+            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) );
+        ABC_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( Aig_Obj_t *, vCompletes, pGate, i )
+        Aig_Regular(pGate)->fMarkA = 1;
+    // select only complete gates
+    vGates = Vec_VecStart( Saig_ManRegNum(pAig) );
+    Vec_VecForEachEntry( Aig_Obj_t *, vGatesAll, pGate, i, k )
+        if ( Aig_Regular(pGate)->fMarkA )
+            Vec_VecPush( vGates, i, pGate );
+    // unlabel complete gates
+    Vec_PtrForEachEntry( Aig_Obj_t *, 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) );
+        ABC_PRT( "Time", clock() - clk );
+    }
+    Vec_PtrFree( vCompletes );
+    return vGates;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/cgt/cgtInt.h b/src/opt/cgt/cgtInt.h
new file mode 100644
index 00000000..1fdbf35f
--- /dev/null
+++ b/src/opt/cgt/cgtInt.h
@@ -0,0 +1,122 @@
+/**CFile****************************************************************
+
+  FileName    [cgtInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Clock gating package.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cgtInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__aig__cgt__cgtInt_h
+#define ABC__aig__cgt__cgtInt_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "src/aig/saig/saig.h"
+#include "src/sat/bsat/satSolver.h"
+#include "src/sat/cnf/cnf.h"
+#include "cgt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Cgt_Man_t_ Cgt_Man_t;
+struct Cgt_Man_t_
+{
+    // user's data
+    Cgt_Par_t *  pPars;          // user's parameters
+    Aig_Man_t *  pAig;           // user's AIG manager
+    // 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
+    sat_solver * pSat;           // SAT solver 
+    Vec_Ptr_t *  vPatts;         // simulation patterns
+    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
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== 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, 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_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 );
+extern void             Cgt_ManStop( Cgt_Man_t * p );
+/*=== cgtSat.c ==========================================================*/
+extern int              Cgt_CheckImplication( Cgt_Man_t * p, Aig_Obj_t * pGate, Aig_Obj_t * pFlop );
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/cgt/cgtMan.c b/src/opt/cgt/cgtMan.c
new file mode 100644
index 00000000..7744226d
--- /dev/null
+++ b/src/opt/cgt/cgtMan.c
@@ -0,0 +1,179 @@
+/**CFile****************************************************************
+
+  FileName    [cgtMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Clock gating package.]
+
+  Synopsis    [Manipulation of clock gating manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cgtMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cgtInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cgt_Man_t * Cgt_ManCreate( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars )
+{
+    Cgt_Man_t * p;
+    // prepare the sequential AIG
+    assert( Saig_ManRegNum(pAig) > 0 );
+    Aig_ManFanoutStart( pAig );
+    Aig_ManSetPioNumbers( pAig );
+    // create interpolation manager
+    p = ABC_ALLOC( Cgt_Man_t, 1 ); 
+    memset( p, 0, sizeof(Cgt_Man_t) );
+    p->pPars      = pPars;
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cgt_ManClean( Cgt_Man_t * p )
+{
+    if ( p->pPart )
+    {
+        Aig_ManStop( p->pPart );
+        p->pPart = NULL;
+    }
+    if ( p->pCnf )
+    {
+        Cnf_DataFree( p->pCnf );
+        p->pCnf = NULL;
+    }
+    if ( p->pSat )
+    {
+        sat_solver_delete( p->pSat );
+        p->pSat = NULL;
+    }
+    if ( p->vPatts )
+    {
+        Vec_PtrFree( p->vPatts );
+        p->vPatts = NULL;
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints stats of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 );
+    ABC_PRT( "Time", p->timeTotal );
+/*
+    p->timeOther = p->timeTotal-p->timeAig-p->timePrepare-p->timeSat-p->timeDecision;
+    ABC_PRTP( "AIG        ", p->timeAig,       p->timeTotal );
+    ABC_PRTP( "Prepare    ", p->timePrepare,   p->timeTotal );
+    ABC_PRTP( "SAT solving", p->timeSat,       p->timeTotal );
+    ABC_PRTP( "  unsat    ", p->timeSatUnsat,  p->timeTotal );
+    ABC_PRTP( "  sat      ", p->timeSatSat,    p->timeTotal );
+    ABC_PRTP( "  undecided", p->timeSatUndec,  p->timeTotal );
+    ABC_PRTP( "Other      ", p->timeOther,     p->timeTotal );
+    ABC_PRTP( "TOTAL      ", p->timeTotal,     p->timeTotal );
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cgt_ManStop( Cgt_Man_t * p )
+{
+    if ( p->pPars->fVerbose )
+        Cgt_ManPrintStats( p );
+    if ( p->pFrame )
+        Aig_ManStop( p->pFrame );
+    Cgt_ManClean( p );
+    Vec_PtrFree( p->vFanout );
+    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 );
+    ABC_FREE( p );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/cgt/cgtSat.c b/src/opt/cgt/cgtSat.c
new file mode 100644
index 00000000..0a2a1daa
--- /dev/null
+++ b/src/opt/cgt/cgtSat.c
@@ -0,0 +1,97 @@
+/**CFile****************************************************************
+
+  FileName    [cgtSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Clock gating package.]
+
+  Synopsis    [Checking implications using SAT.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cgtSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cgtInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Runs equivalence test for the two nodes.]
+
+  Description [Both nodes should be regular and different from each other.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cgt_CheckImplication( Cgt_Man_t * p, Aig_Obj_t * pGate, Aig_Obj_t * pMiter )
+{
+    int nBTLimit = p->pPars->nConfMax;
+    int pLits[2], RetValue, clk;
+    p->nCalls++;
+
+    // sanity checks
+    assert( p->pSat && p->pCnf );
+    assert( !Aig_IsComplement(pMiter) );
+    assert( Aig_Regular(pGate) != pMiter );
+
+    // solve under assumptions
+    // G => !M -- true     G & M -- false
+    pLits[0] = toLitCond( p->pCnf->pVarNums[Aig_Regular(pGate)->Id], Aig_IsComplement(pGate) );
+    pLits[1] = toLitCond( p->pCnf->pVarNums[pMiter->Id], 0 );
+
+clk = clock();
+    RetValue = sat_solver_solve( p->pSat, pLits, pLits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+p->timeSat += clock() - clk;
+    if ( RetValue == l_False )
+    {
+p->timeSatUnsat += clock() - clk;
+        pLits[0] = lit_neg( pLits[0] );
+        pLits[1] = lit_neg( pLits[1] );
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+        sat_solver_compress( p->pSat );
+        p->nCallsUnsat++;
+        return 1;
+    }
+    else if ( RetValue == l_True )
+    {
+p->timeSatSat += clock() - clk;
+        p->nCallsSat++;
+        return 0;
+    }
+    else // if ( RetValue1 == l_Undef )
+    {
+p->timeSatUndec += clock() - clk;
+        p->nCallsUndec++;
+        return -1;
+    }
+    return -2;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/cgt/module.make b/src/opt/cgt/module.make
new file mode 100644
index 00000000..68494e68
--- /dev/null
+++ b/src/opt/cgt/module.make
@@ -0,0 +1,5 @@
+SRC +=    src/opt/cgt/cgtAig.c \
+    src/opt/cgt/cgtCore.c \
+    src/opt/cgt/cgtDecide.c \
+    src/opt/cgt/cgtMan.c \
+    src/opt/cgt/cgtSat.c