ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
resWin.c
Go to the documentation of this file.
1
20
21#include "base/abc/abc.h"
22#include "resInt.h"
23
25
26
30
34
47{
48 Res_Win_t * p;
49 // start the manager
50 p = ABC_ALLOC( Res_Win_t, 1 );
51 memset( p, 0, sizeof(Res_Win_t) );
52 // set internal parameters
53 p->nFanoutLimit = 10;
54 p->nLevTfiMinus = 3;
55 // allocate storage
56 p->vRoots = Vec_PtrAlloc( 256 );
57 p->vLeaves = Vec_PtrAlloc( 256 );
58 p->vBranches = Vec_PtrAlloc( 256 );
59 p->vNodes = Vec_PtrAlloc( 256 );
60 p->vDivs = Vec_PtrAlloc( 256 );
61 p->vMatrix = Vec_VecStart( 128 );
62 return p;
63}
64
77{
78 Vec_PtrFree( p->vRoots );
79 Vec_PtrFree( p->vLeaves );
80 Vec_PtrFree( p->vBranches );
81 Vec_PtrFree( p->vNodes );
82 Vec_PtrFree( p->vDivs );
83 Vec_VecFree( p->vMatrix );
84 ABC_FREE( p );
85}
86
87
88
101{
102 Vec_Ptr_t * vFront;
103 Abc_Obj_t * pObj, * pTemp;
104 int i, k, m;
105
106 assert( p->nWinTfiMax > 0 );
107 assert( Vec_VecSize(p->vMatrix) > p->nWinTfiMax );
108
109 // start matrix with the node
110 Vec_VecClear( p->vMatrix );
111 Vec_VecPush( p->vMatrix, 0, p->pNode );
112 Abc_NtkIncrementTravId( p->pNode->pNtk );
113 Abc_NodeSetTravIdCurrent( p->pNode );
114
115 // collect the leaves (nodes pTemp such that "p->pNode->Level - pTemp->Level > p->nWinTfiMax")
116 Vec_PtrClear( p->vLeaves );
117 Vec_VecForEachLevelStartStop( p->vMatrix, vFront, i, 0, p->nWinTfiMax+1 )
118 {
119 Vec_PtrForEachEntry( Abc_Obj_t *, vFront, pObj, k )
120 {
121 Abc_ObjForEachFanin( pObj, pTemp, m )
122 {
123 if ( Abc_NodeIsTravIdCurrent( pTemp ) )
124 continue;
125 Abc_NodeSetTravIdCurrent( pTemp );
126 if ( Abc_ObjIsCi(pTemp) || (int)(p->pNode->Level - pTemp->Level) > p->nWinTfiMax )
127 Vec_PtrPush( p->vLeaves, pTemp );
128 else
129 Vec_VecPush( p->vMatrix, p->pNode->Level - pTemp->Level, pTemp );
130 }
131 }
132 }
133 if ( Vec_PtrSize(p->vLeaves) == 0 )
134 return 0;
135
136 // collect the nodes in the reverse order
137 Vec_PtrClear( p->vNodes );
138 Vec_VecForEachLevelReverseStartStop( p->vMatrix, vFront, i, p->nWinTfiMax+1, 0 )
139 {
140 Vec_PtrForEachEntry( Abc_Obj_t *, vFront, pObj, k )
141 Vec_PtrPush( p->vNodes, pObj );
142 Vec_PtrClear( vFront );
143 }
144
145 // get the lowest leaf level
146 p->nLevLeafMin = ABC_INFINITY;
147 Vec_PtrForEachEntry( Abc_Obj_t *, p->vLeaves, pObj, k )
148 p->nLevLeafMin = Abc_MinInt( p->nLevLeafMin, (int)pObj->Level );
149
150 // set minimum traversal level
151 p->nLevTravMin = Abc_MaxInt( ((int)p->pNode->Level) - p->nWinTfiMax - p->nLevTfiMinus, p->nLevLeafMin );
152 assert( p->nLevTravMin >= 0 );
153 return 1;
154}
155
156
157
169static inline int Res_WinComputeRootsCheck( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit )
170{
171 Abc_Obj_t * pFanout;
172 int i;
173 // the node is the root if one of the following is true:
174 // (1) the node has more than fanouts than the limit
175 if ( Abc_ObjFanoutNum(pNode) > nFanoutLimit )
176 return 1;
177 // (2) the node has CO fanouts
178 // (3) the node has fanouts above the cutoff level
179 Abc_ObjForEachFanout( pNode, pFanout, i )
180 if ( Abc_ObjIsCo(pFanout) || (int)pFanout->Level > nLevelMax )
181 return 1;
182 return 0;
183}
184
196void Res_WinComputeRoots_rec( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit, Vec_Ptr_t * vRoots )
197{
198 Abc_Obj_t * pFanout;
199 int i;
200 assert( Abc_ObjIsNode(pNode) );
201 if ( Abc_NodeIsTravIdCurrent(pNode) )
202 return;
203 Abc_NodeSetTravIdCurrent( pNode );
204 // check if the node should be the root
205 if ( Res_WinComputeRootsCheck( pNode, nLevelMax, nFanoutLimit ) )
206 Vec_PtrPush( vRoots, pNode );
207 else // if not, explore its fanouts
208 Abc_ObjForEachFanout( pNode, pFanout, i )
209 Res_WinComputeRoots_rec( pFanout, nLevelMax, nFanoutLimit, vRoots );
210}
211
224{
225 Vec_PtrClear( p->vRoots );
226 Abc_NtkIncrementTravId( p->pNode->pNtk );
227 Res_WinComputeRoots_rec( p->pNode, p->pNode->Level + p->nWinTfoMax, p->nFanoutLimit, p->vRoots );
228 assert( Vec_PtrSize(p->vRoots) > 0 );
229 if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode )
230 return 0;
231 return 1;
232}
233
234
235
247int Res_WinMarkPaths_rec( Abc_Obj_t * pNode, Abc_Obj_t * pPivot, int nLevelMin )
248{
249 Abc_Obj_t * pFanin;
250 int i, RetValue;
251 // skip visited nodes
252 if ( Abc_NodeIsTravIdCurrent(pNode) )
253 return 1;
254 if ( Abc_NodeIsTravIdPrevious(pNode) )
255 return 0;
256 // assume that the node does not have access to the leaves
257 Abc_NodeSetTravIdPrevious( pNode );
258 // skip nodes below the given level
259 if ( pNode == pPivot || (int)pNode->Level <= nLevelMin )
260 return 0;
261 assert( Abc_ObjIsNode(pNode) );
262 // check if the fanins have access to the leaves
263 RetValue = 0;
264 Abc_ObjForEachFanin( pNode, pFanin, i )
265 RetValue |= Res_WinMarkPaths_rec( pFanin, pPivot, nLevelMin );
266 // relabel the node if it has access to the leaves
267 if ( RetValue )
268 Abc_NodeSetTravIdCurrent( pNode );
269 return RetValue;
270}
271
284{
285 Abc_Obj_t * pObj;
286 int i;
287 // mark the leaves
288 Abc_NtkIncrementTravId( p->pNode->pNtk );
289 Abc_NtkIncrementTravId( p->pNode->pNtk );
290 Vec_PtrForEachEntry( Abc_Obj_t *, p->vLeaves, pObj, i )
291 Abc_NodeSetTravIdCurrent( pObj );
292 // traverse from the roots and mark the nodes that can reach leaves
293 // the nodes that do not reach leaves have previous trav ID
294 // the nodes that reach leaves have current trav ID
295 Vec_PtrForEachEntry( Abc_Obj_t *, p->vRoots, pObj, i )
296 Res_WinMarkPaths_rec( pObj, p->pNode, p->nLevTravMin );
297}
298
299
300
301
314{
315 Abc_Obj_t * pFanout;
316 int i;
317 assert( Abc_ObjIsNode(pObj) );
318 assert( Abc_NodeIsTravIdCurrent(pObj) );
319 // check if the node has all fanouts marked
320 Abc_ObjForEachFanout( pObj, pFanout, i )
321 if ( !Abc_NodeIsTravIdCurrent(pFanout) )
322 break;
323 // if some of the fanouts are unmarked, add the node to the roots
324 if ( i < Abc_ObjFanoutNum(pObj) )
325 Vec_PtrPushUnique( vRoots, pObj );
326 else // otherwise, call recursively
327 Abc_ObjForEachFanout( pObj, pFanout, i )
328 Res_WinFinalizeRoots_rec( pFanout, vRoots );
329}
330
344{
345 assert( !Abc_NodeIsTravIdCurrent(p->pNode) );
346 // mark the node with the old traversal ID
347 Abc_NodeSetTravIdCurrent( p->pNode );
348 // recollect the roots
349 Vec_PtrClear( p->vRoots );
350 Res_WinFinalizeRoots_rec( p->pNode, p->vRoots );
351 assert( Vec_PtrSize(p->vRoots) > 0 );
352 if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode )
353 return 0;
354 return 1;
355}
356
357
369void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj, int nLevTravMin )
370{
371 Abc_Obj_t * pFanin;
372 int i;
373 // skip the already collected leaves, nodes, and branches
374 if ( Abc_NodeIsTravIdCurrent(pObj) )
375 return;
376 // if this is not an internal node - make it a new branch
377 if ( !Abc_NodeIsTravIdPrevious(pObj) )
378 {
379 assert( Vec_PtrFind(p->vLeaves, pObj) == -1 );
380 Abc_NodeSetTravIdCurrent( pObj );
381 Vec_PtrPush( p->vBranches, pObj );
382 return;
383 }
384 assert( Abc_ObjIsNode(pObj) ); // if this is a CI, then the window is incorrect!
385 Abc_NodeSetTravIdCurrent( pObj );
386 // visit the fanins of the node
387 Abc_ObjForEachFanin( pObj, pFanin, i )
388 Res_WinAddMissing_rec( p, pFanin, nLevTravMin );
389 // collect the node
390 Vec_PtrPush( p->vNodes, pObj );
391}
392
405{
406 Abc_Obj_t * pObj;
407 int i;
408 // mark the leaves
409 Abc_NtkIncrementTravId( p->pNode->pNtk );
410 Vec_PtrForEachEntry( Abc_Obj_t *, p->vLeaves, pObj, i )
411 Abc_NodeSetTravIdCurrent( pObj );
412 // mark the already collected nodes
413 Vec_PtrForEachEntry( Abc_Obj_t *, p->vNodes, pObj, i )
414 Abc_NodeSetTravIdCurrent( pObj );
415 // explore from the roots
416 Vec_PtrClear( p->vBranches );
417 Vec_PtrForEachEntry( Abc_Obj_t *, p->vRoots, pObj, i )
418 Res_WinAddMissing_rec( p, pObj, p->nLevTravMin );
419}
420
421
422
423
436{
437 return Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode;
438}
439
451int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p )
452{
453 assert( Abc_ObjIsNode(pNode) );
454 assert( nWinTfiMax > 0 && nWinTfiMax < 10 );
455 assert( nWinTfoMax >= 0 && nWinTfoMax < 10 );
456
457 // initialize the window
458 p->pNode = pNode;
459 p->nWinTfiMax = nWinTfiMax;
460 p->nWinTfoMax = nWinTfoMax;
461
462 Vec_PtrClear( p->vBranches );
463 Vec_PtrClear( p->vDivs );
464 Vec_PtrClear( p->vRoots );
465 Vec_PtrPush( p->vRoots, pNode );
466
467 // compute the leaves
469 return 0;
470
471 // compute the candidate roots
472 if ( p->nWinTfoMax > 0 && Res_WinComputeRoots(p) )
473 {
474 // mark the paths from the roots to the leaves
476 // refine the roots and add branches and missing nodes
477 if ( Res_WinFinalizeRoots( p ) )
479 }
480
481 return 1;
482}
483
487
488
490
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition abc.h:527
#define Abc_ObjForEachFanout(pObj, pFanout, i)
Definition abc.h:529
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Cube * p
Definition exorList.c:222
typedefABC_NAMESPACE_HEADER_START struct Res_Win_t_ Res_Win_t
INCLUDES ///.
Definition resInt.h:44
void Res_WinAddMissing_rec(Res_Win_t *p, Abc_Obj_t *pObj, int nLevTravMin)
Definition resWin.c:369
int Res_WinComputeRoots(Res_Win_t *p)
Definition resWin.c:223
void Res_WinFinalizeRoots_rec(Abc_Obj_t *pObj, Vec_Ptr_t *vRoots)
Definition resWin.c:313
int Res_WinIsTrivial(Res_Win_t *p)
Definition resWin.c:435
void Res_WinAddMissing(Res_Win_t *p)
Definition resWin.c:404
int Res_WinCompute(Abc_Obj_t *pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t *p)
Definition resWin.c:451
void Res_WinFree(Res_Win_t *p)
Definition resWin.c:76
ABC_NAMESPACE_IMPL_START Res_Win_t * Res_WinAlloc()
DECLARATIONS ///.
Definition resWin.c:46
void Res_WinMarkPaths(Res_Win_t *p)
Definition resWin.c:283
int Res_WinCollectLeavesAndNodes(Res_Win_t *p)
Definition resWin.c:100
int Res_WinMarkPaths_rec(Abc_Obj_t *pNode, Abc_Obj_t *pPivot, int nLevelMin)
Definition resWin.c:247
void Res_WinComputeRoots_rec(Abc_Obj_t *pNode, int nLevelMax, int nFanoutLimit, Vec_Ptr_t *vRoots)
Definition resWin.c:196
int Res_WinFinalizeRoots(Res_Win_t *p)
Definition resWin.c:343
unsigned Level
Definition abc.h:142
#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
#define Vec_VecForEachLevelStartStop(vGlob, vVec, i, LevelStart, LevelStop)
Definition vecVec.h:61
#define Vec_VecForEachLevelReverseStartStop(vGlob, vVec, i, LevelStart, LevelStop)
Definition vecVec.h:65