/**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 "aig/saig/saig.h" #include "sat/bsat/satSolver.h" #include "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 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 // 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 abctime timeAig; // constructing AIG abctime timePrepare; // partitioning and SAT solving abctime timeSat; // total runtime abctime timeSatSat; // satisfiable runtime abctime timeSatUnsat; // unsatisfiable runtime abctime timeSatUndec; // undecided runtime abctime timeDecision; // making decision about what gates to use abctime timeOther; // other runtime abctime timeTotal; // total runtime }; //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// /*=== cgtAig.c ==========================================================*/ 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 ); /*=== 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 /// ////////////////////////////////////////////////////////////////////////