Synchronizing with the recent version.

6 files changed, 29 insertions, 25 deletions

diff --git a/src/opt/cgt/cgt.h b/src/opt/cgt/cgt.h
index 73edbfc3..e92f4e31 100644
--- a/src/opt/cgt/cgt.h
+++ b/src/opt/cgt/cgt.h
@@ -69,7 +69,8 @@ struct Cgt_Par_t_
 
 /*=== 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 Vec_Vec_t *     Cgt_ClockGatingCandidates( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars, Vec_Int_t * vUseful );
+extern Vec_Vec_t *     Cgt_ClockGatingInt( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars, Vec_Int_t * vUseful );
 extern Aig_Man_t *     Cgt_ClockGating( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars );
 
 
diff --git a/src/opt/cgt/cgtAig.c b/src/opt/cgt/cgtAig.c
index 047f6875..9421b75e 100644
--- a/src/opt/cgt/cgtAig.c
+++ b/src/opt/cgt/cgtAig.c
@@ -42,17 +42,17 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void Cgt_ManDetectCandidates_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevelMax, Vec_Ptr_t * vCands )
+void Cgt_ManDetectCandidates_rec( Aig_Man_t * pAig, Vec_Int_t * vUseful, 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 );
+        Cgt_ManDetectCandidates_rec( pAig, vUseful, Aig_ObjFanin0(pObj), nLevelMax, vCands );
+        Cgt_ManDetectCandidates_rec( pAig, vUseful, Aig_ObjFanin1(pObj), nLevelMax, vCands );
     }
-    if ( Aig_ObjLevel(pObj) <= nLevelMax )
+    if ( Aig_ObjLevel(pObj) <= nLevelMax && (vUseful == NULL || Vec_IntEntry(vUseful, Aig_ObjId(pObj))) )
         Vec_PtrPush( vCands, pObj );
 }
 
@@ -67,13 +67,13 @@ void Cgt_ManDetectCandidates_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevel
   SeeAlso     []
 
 ***********************************************************************/
-void Cgt_ManDetectCandidates( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevelMax, Vec_Ptr_t * vCands )
+void Cgt_ManDetectCandidates( Aig_Man_t * pAig, Vec_Int_t * vUseful, 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 );
+    Cgt_ManDetectCandidates_rec( pAig, vUseful, pObj, nLevelMax, vCands );
 }
 
 /**Function*************************************************************
diff --git a/src/opt/cgt/cgtCore.c b/src/opt/cgt/cgtCore.c
index a7b3844c..d87801a3 100644
--- a/src/opt/cgt/cgtCore.c
+++ b/src/opt/cgt/cgtCore.c
@@ -53,7 +53,7 @@ void Cgt_SetDefaultParams( Cgt_Par_t * p )
     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
+    p->fVerbose   =     0;   // verbosity flag
 }
 
 /**Function*************************************************************
@@ -138,7 +138,7 @@ void Cgt_ClockGatingRangeCheck( Cgt_Man_t * p, int iStart, int nOutputs )
     {
         nCalls = p->nCalls;
         pMiter = Saig_ManLi( p->pAig, i );
-        Cgt_ManDetectCandidates( p->pAig, Aig_ObjFanin0(pMiter), p->pPars->nLevelMax, vNodes );
+        Cgt_ManDetectCandidates( p->pAig, p->vUseful, Aig_ObjFanin0(pMiter), p->pPars->nLevelMax, vNodes );
         // go through the candidates of this PO
         Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pCand, k )
         {
@@ -242,7 +242,7 @@ p->timePrepare += Abc_Clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Vec_t * Cgt_ClockGatingCandidates( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars )
+Vec_Vec_t * Cgt_ClockGatingCandidates( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars, Vec_Int_t * vUseful )
 {
     Bar_Progress_t * pProgress = NULL;
     Cgt_Par_t Pars; 
@@ -255,6 +255,7 @@ Vec_Vec_t * Cgt_ClockGatingCandidates( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_
     if ( pPars == NULL )
         Cgt_SetDefaultParams( pPars = &Pars );    
     p = Cgt_ManCreate( pAig, pCare, pPars );
+    p->vUseful = vUseful;
     p->pFrame = Cgt_ManDeriveAigForGating( p );
 p->timeAig += Abc_Clock() - clk;
     assert( Aig_ManCoNum(p->pFrame) == Saig_ManRegNum(p->pAig) );
@@ -283,17 +284,22 @@ p->timeTotal = Abc_Clock() - clkTotal;
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Cgt_ClockGating( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars )
+Vec_Vec_t * Cgt_ClockGatingInt( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars, Vec_Int_t * vUseful )
 {
-    Aig_Man_t * pGated;
-    Vec_Vec_t * vGatesAll;
-    Vec_Vec_t * vGates;
-    int nNodesUsed;//, clk = Abc_Clock();
-    vGatesAll = Cgt_ClockGatingCandidates( pAig, pCare, pPars );
+    Vec_Vec_t * vGatesAll, * vGates;
+    vGatesAll = Cgt_ClockGatingCandidates( pAig, pCare, pPars, vUseful );
     if ( pPars->fAreaOnly )
         vGates = Cgt_ManDecideArea( pAig, vGatesAll, pPars->nOdcMax, pPars->fVerbose );
     else
         vGates = Cgt_ManDecideSimple( pAig, vGatesAll, pPars->nOdcMax, pPars->fVerbose );
+    Vec_VecFree( vGatesAll );
+    return vGates;
+}
+Aig_Man_t * Cgt_ClockGating( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars )
+{
+    Aig_Man_t * pGated;
+    Vec_Vec_t * vGates = Cgt_ClockGatingInt( pAig, pCare, pPars, NULL );
+    int nNodesUsed;
     if ( pPars->fVerbose )
     {
 //        printf( "Before CG: " );
@@ -310,7 +316,6 @@ Aig_Man_t * Cgt_ClockGating( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pP
             Aig_ManNodeNum(pGated) );
     }
     Vec_VecFree( vGates );
-    Vec_VecFree( vGatesAll );
     return pGated;
 }
 
diff --git a/src/opt/cgt/cgtDecide.c b/src/opt/cgt/cgtDecide.c
index 033375a7..ac463b45 100644
--- a/src/opt/cgt/cgtDecide.c
+++ b/src/opt/cgt/cgtDecide.c
@@ -161,15 +161,12 @@ float Cgt_ManComputeCoverage( Aig_Man_t * pAig, Vec_Vec_t * vGates )
     int nWords  =  1;
     Ssw_Sml_t * pSml;
     Vec_Ptr_t * vOne;
-    int i, nTransTotal = 0, nTransSaved = 0;
+    int i, 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;
+    return (float)100.0*nTransSaved/32/nFrames/nWords/Vec_VecSize(vGates);
 }
 
 /**Function*************************************************************
diff --git a/src/opt/cgt/cgtInt.h b/src/opt/cgt/cgtInt.h
index 43d38d8d..72c19d70 100644
--- a/src/opt/cgt/cgtInt.h
+++ b/src/opt/cgt/cgtInt.h
@@ -50,6 +50,7 @@ struct Cgt_Man_t_
     // user's data
     Cgt_Par_t *  pPars;          // user's parameters
     Aig_Man_t *  pAig;           // user's AIG manager
+    Vec_Int_t *  vUseful;        // user's candidate nodes
     // user's constraints
     Aig_Man_t *  pCare;          // constraint cones
     Vec_Vec_t *  vSuppsInv;      // inverse support of the constraints
@@ -94,7 +95,7 @@ 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 void             Cgt_ManDetectCandidates( Aig_Man_t * pAig, Vec_Int_t * vUseful, 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 );
diff --git a/src/proof/ssw/sswSim.c b/src/proof/ssw/sswSim.c
index c458855d..e1bcc149 100644
--- a/src/proof/ssw/sswSim.c
+++ b/src/proof/ssw/sswSim.c
@@ -321,7 +321,7 @@ int Ssw_SmlNodeIsZeroFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f )
 
 /**Function*************************************************************
 
-  Synopsis    [Counts the number of one's in the patten the object.]
+  Synopsis    [Counts the number of one's in the pattern of the object.]
 
   Description []
 
@@ -350,7 +350,7 @@ int Ssw_SmlNodeCountOnesReal( Ssw_Sml_t * p, Aig_Obj_t * pObj )
 
 /**Function*************************************************************
 
-  Synopsis    [Counts the number of one's in the patten the object.]
+  Synopsis    [Counts the number of one's in the pattern of the objects.]
 
   Description []