summaryrefslogtreecommitdiffstats
path: root/src/aig/cgt
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/cgt')
-rw-r--r--src/aig/cgt/cgt.h81
-rw-r--r--src/aig/cgt/cgtAig.c311
-rw-r--r--src/aig/cgt/cgtCore.c254
-rw-r--r--src/aig/cgt/cgtDecide.c102
-rw-r--r--src/aig/cgt/cgtInt.h107
-rw-r--r--src/aig/cgt/cgtMan.c168
-rw-r--r--src/aig/cgt/cgtSat.c92
-rw-r--r--src/aig/cgt/module.make5
8 files changed, 1120 insertions, 0 deletions
diff --git a/src/aig/cgt/cgt.h b/src/aig/cgt/cgt.h
new file mode 100644
index 00000000..b9997d56
--- /dev/null
+++ b/src/aig/cgt/cgt.h
@@ -0,0 +1,81 @@
+/**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 __CGT_H__
+#define __CGT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/*
+ 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 ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// 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 fVerbose; // 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 );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/cgt/cgtAig.c b/src/aig/cgt/cgtAig.c
new file mode 100644
index 00000000..b30d3f16
--- /dev/null
+++ b/src/aig/cgt/cgtAig.c
@@ -0,0 +1,311 @@
+/**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"
+
+////////////////////////////////////////////////////////////////////////
+/// 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(Aig_ObjFanin0(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( 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, Aig_ObjCompareIdIncrease );
+ assert( Vec_PtrSize(vFanout) > 0 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives miter for clock-gating.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Cgt_ManConstructMiter( Cgt_Man_t * p, Aig_Man_t * pNew, Aig_Obj_t * pObjLo )
+{
+ Aig_Obj_t * pMiter, * pRoot;
+ int i;
+ assert( Aig_ObjIsPi(pObjLo) );
+ pMiter = Aig_ManConst0( pNew );
+ 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) );
+ 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;
+ int i;
+ assert( Aig_ManRegNum(p->pAig) );
+ Aig_ManCleanNext( p->pAig );
+ pNew = Aig_ManStart( Aig_ManObjNumMax(p->pAig) );
+ // 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) );
+ // 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 );
+ Aig_ManCleanup( pNew );
+ return pNew;
+}
+
+/**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 )
+{
+ 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) );
+ return 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 * pAig, int nVarsMin, int nFlopsMin, int iStart )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj;
+ int i;
+ assert( Aig_ManRegNum(pAig) == 0 );
+ 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++ )
+ {
+ pObj = Aig_ManPo( pAig, i );
+ Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
+ pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ }
+ for ( ; Aig_ManObjNum(pNew) < nVarsMin && i < Aig_ManPoNum(pAig); i++ )
+ {
+ pObj = Aig_ManPo( pAig, i );
+ Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
+ pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ }
+ assert( nFlopsMin >= Aig_ManPoNum(pAig) || Aig_ManPoNum(pNew) >= nFlopsMin );
+ return pNew;
+}
+
+/**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_Ptr_t * vGates )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo, * pGate, * pGateNew;
+ int i;
+ assert( Aig_ManRegNum(pAig) );
+ pNew = Aig_ManStart( Aig_ManObjNumMax(pAig) );
+ 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) );
+ 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 )
+ pObjNew = Aig_ObjChild0Copy(pObjLi);
+ else
+ {
+ pGateNew = Aig_NotCond( Aig_Regular(pGate)->pData, Aig_IsComplement(pGate) );
+ 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) );
+ return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cgt/cgtCore.c b/src/aig/cgt/cgtCore.c
new file mode 100644
index 00000000..a06820b4
--- /dev/null
+++ b/src/aig/cgt/cgtCore.c
@@ -0,0 +1,254 @@
+/**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"
+
+////////////////////////////////////////////////////////////////////////
+/// 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 = 1000; // 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
+}
+
+/**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 * pCandFrame, Aig_Obj_t * pMiterFrame )
+{
+ 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) );
+ // C => !M -- true is the same as C & M -- false
+ if ( !Aig_IsComplement(pCandFrame) )
+ {
+ 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] ) )
+ Aig_InfoSetBit( Vec_PtrEntry(p->vPatts, i), p->nPatts );
+ p->nPatts++;
+ if ( p->nPatts == 32 * p->nPattWords )
+ {
+ Vec_PtrReallocSimInfo( p->vPatts );
+ p->nPattWords *= 2;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs clock-gating for the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cgt_ClockGatingRangeCheck( Cgt_Man_t * p, int iStart )
+{
+ Vec_Ptr_t * vNodes = p->vFanout;
+ Aig_Obj_t * pMiter, * pCand, * pMiterFrame, * pCandFrame, * pMiterPart, * pCandPart;
+ int i, k, RetValue;
+ 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++ )
+ {
+ 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( vNodes, pCand, k )
+ {
+ // get the corresponding nodes from the frames
+ pCandFrame = pCand->pData;
+ pMiterFrame = pMiter->pData;
+ // get the corresponding nodes from the part
+ pCandPart = pCandFrame->pData;
+ pMiterPart = 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 );
+ }
+ // 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 );
+ }
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs clock-gating for the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+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) );
+ p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
+ sat_solver_compress( p->pSat );
+ p->vPatts = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pPart), 16 );
+ Vec_PtrCleanSimInfo( p->vPatts, 0, p->nPattWords );
+ Cgt_ClockGatingRangeCheck( p, iStart );
+ iStop = iStart + Aig_ManPoNum(p->pPart);
+ Cgt_ManClean( p );
+ 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 )
+{
+ Cgt_Par_t Pars;
+ Cgt_Man_t * p;
+ Vec_Vec_t * vGatesAll;
+ int iStart;
+ if ( pPars == NULL )
+ Cgt_SetDefaultParams( pPars = &Pars );
+ p = Cgt_ManCreate( pAig, pCare, pPars );
+ p->pFrame = Cgt_ManDeriveAigForGating( p );
+ assert( Aig_ManPoNum(p->pFrame) == Saig_ManRegNum(p->pAig) );
+ for ( iStart = 0; iStart < Aig_ManPoNum(p->pFrame); )
+ iStart = Cgt_ClockGatingRange( p, iStart );
+ vGatesAll = p->vGatesAll;
+ 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_Ptr_t * vGates;
+ vGatesAll = Cgt_ClockGatingCandidates( pAig, pCare, pPars );
+ vGates = Cgt_ManDecideSimple( pAig, vGatesAll );
+ pGated = Cgt_ManDeriveGatedAig( pAig, vGates );
+ Vec_PtrFree( vGates );
+ Vec_VecFree( vGatesAll );
+ return pGated;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cgt/cgtDecide.c b/src/aig/cgt/cgtDecide.c
new file mode 100644
index 00000000..8f57bd4a
--- /dev/null
+++ b/src/aig/cgt/cgtDecide.c
@@ -0,0 +1,102 @@
+/**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 "sswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// 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 );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Chooses what clock-gate to use for each register.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Cgt_ManDecide( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll )
+{
+ Vec_Ptr_t * vGates;
+ vGates = Vec_PtrStart( Saig_ManRegNum(pAig) );
+ return vGates;
+}
+
+/**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_Ptr_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll )
+{
+ Ssw_Sml_t * pSml;
+ Vec_Ptr_t * vGates, * 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 );
+ Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
+ {
+ nHitsMax = 0;
+ pCandBest = NULL;
+ vCands = Vec_VecEntry( vGatesAll, i );
+ Vec_PtrForEachEntry( vCands, pCand, k )
+ {
+ // check if this is indeed a clock-gate
+ if ( !Ssw_SmlCheckXorImplication( pSml, pObjLi, pObjLo, pCand ) )
+ printf( "Clock gate candidate is invalid!\n" );
+ // find its characteristic number
+ nHitsCur = Ssw_SmlCountXorImplication( pSml, pObjLi, pObjLo, pCand );
+ if ( nHitsMax < nHitsCur )
+ {
+ nHitsMax = nHitsCur;
+ pCandBest = pCand;
+ }
+ }
+ if ( pCandBest != NULL )
+ Vec_PtrWriteEntry( vGates, i, pCandBest );
+ }
+ Ssw_SmlStop( pSml );
+ return vGates;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cgt/cgtInt.h b/src/aig/cgt/cgtInt.h
new file mode 100644
index 00000000..7b4b6e63
--- /dev/null
+++ b/src/aig/cgt/cgtInt.h
@@ -0,0 +1,107 @@
+/**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 __CGT_INT_H__
+#define __CGT_INT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include "saig.h"
+#include "satSolver.h"
+#include "cnf.h"
+#include "cgt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// 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
+ Aig_Man_t * pCare; // user's constraints
+ 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
+ // 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 nCalls; // total calls
+ int nCallsSat; // satisfiable calls
+ int nCallsUnsat; // unsatisfiable calls
+ int nCallsUndec; // undecided calls
+ int timeSat; // total runtime
+ int timeSatSat; // satisfiable runtime
+ int timeSatUnsat; // unsatisfiable runtime
+ int timeSatUndec; // undecided 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 );
+extern Aig_Man_t * Cgt_ManDeriveGatedAig( Aig_Man_t * pAig, Vec_Ptr_t * vGates );
+/*=== 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 );
+/*=== 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 );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/cgt/cgtMan.c b/src/aig/cgt/cgtMan.c
new file mode 100644
index 00000000..9615d2e6
--- /dev/null
+++ b/src/aig/cgt/cgtMan.c
@@ -0,0 +1,168 @@
+/**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"
+
+////////////////////////////////////////////////////////////////////////
+/// 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 = 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->nPattWords = 16;
+ 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 )
+{
+/*
+ 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 );
+ PRTP( "SAT solving", p->timeSat, p->timeTotal );
+ PRTP( " unsat ", p->timeSatUnsat, p->timeTotal );
+ PRTP( " sat ", p->timeSatSat, p->timeTotal );
+ PRTP( " undecided", p->timeSatUndec, p->timeTotal );
+ PRTP( "Other ", p->timeOther, p->timeTotal );
+ 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->vGates );
+ Vec_VecFree( p->vGatesAll );
+ free( p );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cgt/cgtSat.c b/src/aig/cgt/cgtSat.c
new file mode 100644
index 00000000..094fb47d
--- /dev/null
+++ b/src/aig/cgt/cgtSat.c
@@ -0,0 +1,92 @@
+/**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"
+
+////////////////////////////////////////////////////////////////////////
+/// 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, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cgt/module.make b/src/aig/cgt/module.make
new file mode 100644
index 00000000..911d8d1f
--- /dev/null
+++ b/src/aig/cgt/module.make
@@ -0,0 +1,5 @@
+SRC += src/aig/cgt/cgtAig.c \
+ src/aig/cgt/cgtCore.c \
+ src/aig/cgt/cgtDecide.c \
+ src/aig/cgt/cgtMan.c \
+ src/aig/cgt/cgtSat.c
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-05 00:04:02 +0000