| /**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 /// |
| //////////////////////////////////////////////////////////////////////// |
| |
