72 unsigned * pInfoCand, * pInfoMiter;
73 int w,
nWords = Abc_BitWordNum(
p->nPatts );
74 pInfoCand = (
unsigned *)Vec_PtrEntry(
p->vPatts, Aig_ObjId(Aig_Regular(pCandPart)) );
75 pInfoMiter = (
unsigned *)Vec_PtrEntry(
p->vPatts, Aig_ObjId(pMiterPart) );
77 if ( !Aig_IsComplement(pCandPart) )
79 for ( w = 0; w <
nWords; w++ )
80 if ( pInfoCand[w] & pInfoMiter[w] )
85 for ( w = 0; w <
nWords; w++ )
86 if ( ~pInfoCand[w] & pInfoMiter[w] )
108 if ( sat_solver_var_value(
p->pSat,
p->pCnf->pVarNums[i] ) )
109 Abc_InfoSetBit( (
unsigned *)Vec_PtrEntry(
p->vPatts, i),
p->nPatts );
111 if (
p->nPatts == 32 *
p->nPattWords )
113 Vec_PtrReallocSimInfo(
p->vPatts );
114 Vec_PtrCleanSimInfo(
p->vPatts,
p->nPattWords, 2 *
p->nPattWords );
133 Aig_Obj_t * pMiter, * pCand, * pMiterFrame, * pCandFrame, * pMiterPart, * pCandPart;
134 int i, k, RetValue, nCalls;
135 assert( Vec_VecSize(
p->vGatesAll) == Aig_ManCoNum(
p->pFrame) );
137 for ( i = iStart; i < iStart + nOutputs; i++ )
140 pMiter = Saig_ManLi(
p->pAig, i );
157 Vec_VecPush(
p->vGatesAll, i, pCand );
171 Vec_VecPush(
p->vGatesAll, i, Aig_Not(pCand) );
181 if (
p->pPars->fVerbose )
204 abctime clk, clkTotal = Abc_Clock();
205 int nCallsUnsat =
p->nCallsUnsat;
206 int nCallsSat =
p->nCallsSat;
207 int nCallsUndec =
p->nCallsUndec;
208 int nCallsFiltered =
p->nCallsFiltered;
210 p->pPart =
Cgt_ManDupPartition(
p->pFrame,
p->pPars->nVarsMin,
p->pPars->nFlopsMin, iStart,
p->pCare,
p->vSuppsInv, &nOutputs );
213 sat_solver_compress(
p->pSat );
214 p->vPatts = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(
p->pPart),
p->nPattWords );
215 Vec_PtrCleanSimInfo(
p->vPatts, 0,
p->nPattWords );
216p->timePrepare += Abc_Clock() - clk;
218 iStop = iStart + nOutputs;
219 if (
p->pPars->fVeryVerbose )
221 printf(
"%5d : D =%4d. C =%5d. Var =%6d. Pr =%5d. Cex =%5d. F =%4d. Saved =%6d. ",
222 iStart, iStop-iStart, Aig_ManCoNum(
p->pPart)-nOutputs,
p->pSat->size,
223 p->nCallsUnsat-nCallsUnsat,
224 p->nCallsSat -nCallsSat,
225 p->nCallsUndec-nCallsUndec,
226 p->nCallsFiltered-nCallsFiltered );
227 ABC_PRT(
"Time", Abc_Clock() - clkTotal );
252 abctime clk = Abc_Clock(), clkTotal = Abc_Clock();
258 p->vUseful = vUseful;
260p->timeAig += Abc_Clock() - clk;
261 assert( Aig_ManCoNum(
p->pFrame) == Saig_ManRegNum(
p->pAig) );
263 for ( iStart = 0; iStart < Aig_ManCoNum(
p->pFrame); )
265 Bar_ProgressUpdate( pProgress, iStart, NULL );
269 vGatesAll =
p->vGatesAll;
271p->timeTotal = Abc_Clock() - clkTotal;
291 if ( pPars->fAreaOnly )
295 Vec_VecFree( vGatesAll );
303 if ( pPars->fVerbose )
309 if ( pPars->fVerbose )
313 printf(
"Nodes: Before CG = %6d. After CG = %6d. (%6.2f %%). Total after CG = %6d.\n",
314 Aig_ManNodeNum(pAig), nNodesUsed,
315 100.0*nNodesUsed/Aig_ManNodeNum(pAig),
316 Aig_ManNodeNum(pGated) );
318 Vec_VecFree( vGates );
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
#define Aig_ManForEachObj(p, pObj, i)
struct Aig_Obj_t_ Aig_Obj_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
unsigned Aig_ManRandom(int fReset)
void Bar_ProgressStop(Bar_Progress_t *p)
Bar_Progress_t * Bar_ProgressStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
struct Bar_Progress_t_ Bar_Progress_t
BASIC TYPES ///.
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
void Cgt_ManDetectCandidates(Aig_Man_t *pAig, Vec_Int_t *vUseful, Aig_Obj_t *pObj, int nLevelMax, Vec_Ptr_t *vCands)
MACRO DEFINITIONS ///.
Aig_Man_t * Cgt_ManDeriveGatedAig(Aig_Man_t *pAig, Vec_Vec_t *vGates, int fReduce, int *pnUsedNodes)
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)
Aig_Man_t * Cgt_ManDeriveAigForGating(Cgt_Man_t *p)
ABC_NAMESPACE_IMPL_START void Cgt_SetDefaultParams(Cgt_Par_t *p)
DECLARATIONS ///.
int Cgt_SimulationFilter(Cgt_Man_t *p, Aig_Obj_t *pCandPart, Aig_Obj_t *pMiterPart)
void Cgt_ClockGatingRangeCheck(Cgt_Man_t *p, int iStart, int nOutputs)
Vec_Vec_t * Cgt_ClockGatingCandidates(Aig_Man_t *pAig, Aig_Man_t *pCare, Cgt_Par_t *pPars, Vec_Int_t *vUseful)
Vec_Vec_t * Cgt_ClockGatingInt(Aig_Man_t *pAig, Aig_Man_t *pCare, Cgt_Par_t *pPars, Vec_Int_t *vUseful)
Aig_Man_t * Cgt_ClockGating(Aig_Man_t *pAig, Aig_Man_t *pCare, Cgt_Par_t *pPars)
void Cgt_SimulationRecord(Cgt_Man_t *p)
int Cgt_ClockGatingRange(Cgt_Man_t *p, int iStart)
Vec_Vec_t * Cgt_ManDecideSimple(Aig_Man_t *pAig, Vec_Vec_t *vGatesAll, int nOdcMax, int fVerbose)
Vec_Vec_t * Cgt_ManDecideArea(Aig_Man_t *pAig, Vec_Vec_t *vGatesAll, int nOdcMax, int fVerbose)
typedefABC_NAMESPACE_HEADER_START struct Cgt_Man_t_ Cgt_Man_t
INCLUDES ///.
void Cgt_ManClean(Cgt_Man_t *p)
Cgt_Man_t * Cgt_ManCreate(Aig_Man_t *pAig, Aig_Man_t *pCare, Cgt_Par_t *pPars)
DECLARATIONS ///.
void Cgt_ManStop(Cgt_Man_t *p)
int Cgt_CheckImplication(Cgt_Man_t *p, Aig_Obj_t *pGate, Aig_Obj_t *pFlop)
DECLARATIONS ///.
typedefABC_NAMESPACE_HEADER_START struct Cgt_Par_t_ Cgt_Par_t
INCLUDES ///.
Cnf_Dat_t * Cnf_DeriveSimple(Aig_Man_t *p, int nOutputs)
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.