ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
cgtCore.c
Go to the documentation of this file.
1
20
21#include "cgtInt.h"
22#include "misc/bar/bar.h"
23
25
26
30
34
47{
48 memset( p, 0, sizeof(Cgt_Par_t) );
49 p->nLevelMax = 25; // the max number of levels to look for clock-gates
50 p->nCandMax = 1000; // the max number of candidates at each node
51 p->nOdcMax = 0; // the max number of ODC levels to consider
52 p->nConfMax = 10; // the max number of conflicts at a node
53 p->nVarsMin = 1000; // the min number of vars to recycle the SAT solver
54 p->nFlopsMin = 10; // the min number of flops to recycle the SAT solver
55 p->fAreaOnly = 0; // derive clock-gating to minimize area
56 p->fVerbose = 0; // verbosity flag
57}
58
70int Cgt_SimulationFilter( Cgt_Man_t * p, Aig_Obj_t * pCandPart, Aig_Obj_t * pMiterPart )
71{
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) );
76 // C => !M -- true is the same as C & M -- false
77 if ( !Aig_IsComplement(pCandPart) )
78 {
79 for ( w = 0; w < nWords; w++ )
80 if ( pInfoCand[w] & pInfoMiter[w] )
81 return 0;
82 }
83 else
84 {
85 for ( w = 0; w < nWords; w++ )
86 if ( ~pInfoCand[w] & pInfoMiter[w] )
87 return 0;
88 }
89 return 1;
90}
91
104{
105 Aig_Obj_t * pObj;
106 int i;
107 Aig_ManForEachObj( p->pPart, pObj, i )
108 if ( sat_solver_var_value( p->pSat, p->pCnf->pVarNums[i] ) )
109 Abc_InfoSetBit( (unsigned *)Vec_PtrEntry(p->vPatts, i), p->nPatts );
110 p->nPatts++;
111 if ( p->nPatts == 32 * p->nPattWords )
112 {
113 Vec_PtrReallocSimInfo( p->vPatts );
114 Vec_PtrCleanSimInfo( p->vPatts, p->nPattWords, 2 * p->nPattWords );
115 p->nPattWords *= 2;
116 }
117}
118
130void Cgt_ClockGatingRangeCheck( Cgt_Man_t * p, int iStart, int nOutputs )
131{
132 Vec_Ptr_t * vNodes = p->vFanout;
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) );
136 // go through all the registers inputs of this range
137 for ( i = iStart; i < iStart + nOutputs; i++ )
138 {
139 nCalls = p->nCalls;
140 pMiter = Saig_ManLi( p->pAig, i );
141 Cgt_ManDetectCandidates( p->pAig, p->vUseful, Aig_ObjFanin0(pMiter), p->pPars->nLevelMax, vNodes );
142 // go through the candidates of this PO
143 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pCand, k )
144 {
145 // get the corresponding nodes from the frames
146 pCandFrame = (Aig_Obj_t *)pCand->pData;
147 pMiterFrame = (Aig_Obj_t *)pMiter->pData;
148 // get the corresponding nodes from the part
149 pCandPart = (Aig_Obj_t *)pCandFrame->pData;
150 pMiterPart = (Aig_Obj_t *)pMiterFrame->pData;
151 // try direct polarity
152 if ( Cgt_SimulationFilter( p, pCandPart, pMiterPart ) )
153 {
154 RetValue = Cgt_CheckImplication( p, pCandPart, pMiterPart );
155 if ( RetValue == 1 )
156 {
157 Vec_VecPush( p->vGatesAll, i, pCand );
158 continue;
159 }
160 if ( RetValue == 0 )
162 }
163 else
164 p->nCallsFiltered++;
165 // try reverse polarity
166 if ( Cgt_SimulationFilter( p, Aig_Not(pCandPart), pMiterPart ) )
167 {
168 RetValue = Cgt_CheckImplication( p, Aig_Not(pCandPart), pMiterPart );
169 if ( RetValue == 1 )
170 {
171 Vec_VecPush( p->vGatesAll, i, Aig_Not(pCand) );
172 continue;
173 }
174 if ( RetValue == 0 )
176 }
177 else
178 p->nCallsFiltered++;
179 }
180
181 if ( p->pPars->fVerbose )
182 {
183// printf( "Flop %3d : Cand = %4d. Gate = %4d. SAT calls = %3d.\n",
184// i, Vec_PtrSize(vNodes), Vec_PtrSize(Vec_VecEntry(p->vGatesAll, i)), p->nCalls-nCalls );
185 }
186
187 }
188}
189
201int Cgt_ClockGatingRange( Cgt_Man_t * p, int iStart )
202{
203 int nOutputs, iStop;
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;
209clk = Abc_Clock();
210 p->pPart = Cgt_ManDupPartition( p->pFrame, p->pPars->nVarsMin, p->pPars->nFlopsMin, iStart, p->pCare, p->vSuppsInv, &nOutputs );
211 p->pCnf = Cnf_DeriveSimple( p->pPart, nOutputs );
212 p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
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;
217 Cgt_ClockGatingRangeCheck( p, iStart, nOutputs );
218 iStop = iStart + nOutputs;
219 if ( p->pPars->fVeryVerbose )
220 {
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 );
228 }
229 Cgt_ManClean( p );
230 p->nRecycles++;
231 return iStop;
232}
233
246{
247 Bar_Progress_t * pProgress = NULL;
248 Cgt_Par_t Pars;
249 Cgt_Man_t * p;
250 Vec_Vec_t * vGatesAll;
251 int iStart;
252 abctime clk = Abc_Clock(), clkTotal = Abc_Clock();
253 // reset random numbers
254 Aig_ManRandom( 1 );
255 if ( pPars == NULL )
256 Cgt_SetDefaultParams( pPars = &Pars );
257 p = Cgt_ManCreate( pAig, pCare, pPars );
258 p->vUseful = vUseful;
259 p->pFrame = Cgt_ManDeriveAigForGating( p );
260p->timeAig += Abc_Clock() - clk;
261 assert( Aig_ManCoNum(p->pFrame) == Saig_ManRegNum(p->pAig) );
262 pProgress = Bar_ProgressStart( stdout, Aig_ManCoNum(p->pFrame) );
263 for ( iStart = 0; iStart < Aig_ManCoNum(p->pFrame); )
264 {
265 Bar_ProgressUpdate( pProgress, iStart, NULL );
266 iStart = Cgt_ClockGatingRange( p, iStart );
267 }
268 Bar_ProgressStop( pProgress );
269 vGatesAll = p->vGatesAll;
270 p->vGatesAll = NULL;
271p->timeTotal = Abc_Clock() - clkTotal;
272 Cgt_ManStop( p );
273 return vGatesAll;
274}
275
287Vec_Vec_t * Cgt_ClockGatingInt( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars, Vec_Int_t * vUseful )
288{
289 Vec_Vec_t * vGatesAll, * vGates;
290 vGatesAll = Cgt_ClockGatingCandidates( pAig, pCare, pPars, vUseful );
291 if ( pPars->fAreaOnly )
292 vGates = Cgt_ManDecideArea( pAig, vGatesAll, pPars->nOdcMax, pPars->fVerbose );
293 else
294 vGates = Cgt_ManDecideSimple( pAig, vGatesAll, pPars->nOdcMax, pPars->fVerbose );
295 Vec_VecFree( vGatesAll );
296 return vGates;
297}
299{
300 Aig_Man_t * pGated;
301 Vec_Vec_t * vGates = Cgt_ClockGatingInt( pAig, pCare, pPars, NULL );
302 int nNodesUsed;
303 if ( pPars->fVerbose )
304 {
305// printf( "Before CG: " );
306// Aig_ManPrintStats( pAig );
307 }
308 pGated = Cgt_ManDeriveGatedAig( pAig, vGates, pPars->fAreaOnly, &nNodesUsed );
309 if ( pPars->fVerbose )
310 {
311// printf( "After CG: " );
312// Aig_ManPrintStats( pGated );
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) );
317 }
318 Vec_VecFree( vGates );
319 return pGated;
320}
321
325
326
328
int nWords
Definition abcNpn.c:127
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_PRT(a, t)
Definition abc_global.h:255
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
#define Aig_ManForEachObj(p, pObj, i)
Definition aig.h:403
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
unsigned Aig_ManRandom(int fReset)
Definition aigUtil.c:1170
void Bar_ProgressStop(Bar_Progress_t *p)
Definition bar.c:126
Bar_Progress_t * Bar_ProgressStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition bar.c:66
struct Bar_Progress_t_ Bar_Progress_t
BASIC TYPES ///.
Definition bar.h:48
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
#define sat_solver
Definition cecSatG2.c:34
void Cgt_ManDetectCandidates(Aig_Man_t *pAig, Vec_Int_t *vUseful, Aig_Obj_t *pObj, int nLevelMax, Vec_Ptr_t *vCands)
MACRO DEFINITIONS ///.
Definition cgtAig.c:70
Aig_Man_t * Cgt_ManDeriveGatedAig(Aig_Man_t *pAig, Vec_Vec_t *vGates, int fReduce, int *pnUsedNodes)
Definition cgtAig.c:524
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)
Definition cgtAig.c:441
Aig_Man_t * Cgt_ManDeriveAigForGating(Cgt_Man_t *p)
Definition cgtAig.c:266
ABC_NAMESPACE_IMPL_START void Cgt_SetDefaultParams(Cgt_Par_t *p)
DECLARATIONS ///.
Definition cgtCore.c:46
int Cgt_SimulationFilter(Cgt_Man_t *p, Aig_Obj_t *pCandPart, Aig_Obj_t *pMiterPart)
Definition cgtCore.c:70
void Cgt_ClockGatingRangeCheck(Cgt_Man_t *p, int iStart, int nOutputs)
Definition cgtCore.c:130
Vec_Vec_t * Cgt_ClockGatingCandidates(Aig_Man_t *pAig, Aig_Man_t *pCare, Cgt_Par_t *pPars, Vec_Int_t *vUseful)
Definition cgtCore.c:245
Vec_Vec_t * Cgt_ClockGatingInt(Aig_Man_t *pAig, Aig_Man_t *pCare, Cgt_Par_t *pPars, Vec_Int_t *vUseful)
Definition cgtCore.c:287
Aig_Man_t * Cgt_ClockGating(Aig_Man_t *pAig, Aig_Man_t *pCare, Cgt_Par_t *pPars)
Definition cgtCore.c:298
void Cgt_SimulationRecord(Cgt_Man_t *p)
Definition cgtCore.c:103
int Cgt_ClockGatingRange(Cgt_Man_t *p, int iStart)
Definition cgtCore.c:201
Vec_Vec_t * Cgt_ManDecideSimple(Aig_Man_t *pAig, Vec_Vec_t *vGatesAll, int nOdcMax, int fVerbose)
Definition cgtDecide.c:184
Vec_Vec_t * Cgt_ManDecideArea(Aig_Man_t *pAig, Vec_Vec_t *vGatesAll, int nOdcMax, int fVerbose)
Definition cgtDecide.c:255
typedefABC_NAMESPACE_HEADER_START struct Cgt_Man_t_ Cgt_Man_t
INCLUDES ///.
Definition cgtInt.h:47
void Cgt_ManClean(Cgt_Man_t *p)
Definition cgtMan.c:86
Cgt_Man_t * Cgt_ManCreate(Aig_Man_t *pAig, Aig_Man_t *pCare, Cgt_Par_t *pPars)
DECLARATIONS ///.
Definition cgtMan.c:45
void Cgt_ManStop(Cgt_Man_t *p)
Definition cgtMan.c:154
int Cgt_CheckImplication(Cgt_Man_t *p, Aig_Obj_t *pGate, Aig_Obj_t *pFlop)
DECLARATIONS ///.
Definition cgtSat.c:46
typedefABC_NAMESPACE_HEADER_START struct Cgt_Par_t_ Cgt_Par_t
INCLUDES ///.
Definition cgt.h:48
Cnf_Dat_t * Cnf_DeriveSimple(Aig_Man_t *p, int nOutputs)
Definition cnfWrite.c:587
Cube * p
Definition exorList.c:222
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition cnfMan.c:579
void * pData
Definition aig.h:87
#define assert(ex)
Definition util_old.h:213
char * memset()
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42