ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
hopDfs.c
Go to the documentation of this file.
1
20
21#include "hop.h"
22
24
25
29
33
45void Hop_ManDfs_rec( Hop_Obj_t * pObj, Vec_Ptr_t * vNodes )
46{
47 assert( !Hop_IsComplement(pObj) );
48 if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
49 return;
50 Hop_ManDfs_rec( Hop_ObjFanin0(pObj), vNodes );
51 Hop_ManDfs_rec( Hop_ObjFanin1(pObj), vNodes );
52 assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
53 Hop_ObjSetMarkA(pObj);
54 Vec_PtrPush( vNodes, pObj );
55}
56
69{
70 Vec_Ptr_t * vNodes;
71 Hop_Obj_t * pObj;
72 int i;
73 vNodes = Vec_PtrAlloc( Hop_ManNodeNum(p) );
74 Hop_ManForEachNode( p, pObj, i )
75 Hop_ManDfs_rec( pObj, vNodes );
76 Hop_ManForEachNode( p, pObj, i )
77 Hop_ObjClearMarkA(pObj);
78 return vNodes;
79}
80
93{
94 Vec_Ptr_t * vNodes;
95 Hop_Obj_t * pObj;
96 int i;
97 assert( !Hop_IsComplement(pNode) );
98 vNodes = Vec_PtrAlloc( 16 );
99 Hop_ManDfs_rec( pNode, vNodes );
100 Vec_PtrForEachEntry( Hop_Obj_t *, vNodes, pObj, i )
101 Hop_ObjClearMarkA(pObj);
102 return vNodes;
103}
104
117{
118 Vec_Ptr_t * vNodes;
119 Hop_Obj_t * pObj;
120 int i, LevelsMax, Level0, Level1;
121 // initialize the levels
122 Hop_ManConst1(p)->pData = NULL;
123 Hop_ManForEachPi( p, pObj, i )
124 pObj->pData = NULL;
125 // compute levels in a DFS order
126 vNodes = Hop_ManDfs( p );
127 Vec_PtrForEachEntry( Hop_Obj_t *, vNodes, pObj, i )
128 {
129 Level0 = (int)(ABC_PTRUINT_T)Hop_ObjFanin0(pObj)->pData;
130 Level1 = (int)(ABC_PTRUINT_T)Hop_ObjFanin1(pObj)->pData;
131 pObj->pData = (void *)(ABC_PTRUINT_T)(1 + Hop_ObjIsExor(pObj) + Abc_MaxInt(Level0, Level1));
132 }
133 Vec_PtrFree( vNodes );
134 // get levels of the POs
135 LevelsMax = 0;
136 Hop_ManForEachPo( p, pObj, i )
137 LevelsMax = Abc_MaxInt( LevelsMax, (int)(ABC_PTRUINT_T)Hop_ObjFanin0(pObj)->pData );
138 return LevelsMax;
139}
140
153{
154 Hop_Obj_t * pObj;
155 int i;
156 if ( p->fRefCount )
157 return;
158 p->fRefCount = 1;
159 // clear refs
160 Hop_ObjClearRef( Hop_ManConst1(p) );
161 Hop_ManForEachPi( p, pObj, i )
162 Hop_ObjClearRef( pObj );
163 Hop_ManForEachNode( p, pObj, i )
164 Hop_ObjClearRef( pObj );
165 Hop_ManForEachPo( p, pObj, i )
166 Hop_ObjClearRef( pObj );
167 // set refs
168 Hop_ManForEachNode( p, pObj, i )
169 {
170 Hop_ObjRef( Hop_ObjFanin0(pObj) );
171 Hop_ObjRef( Hop_ObjFanin1(pObj) );
172 }
173 Hop_ManForEachPo( p, pObj, i )
174 Hop_ObjRef( Hop_ObjFanin0(pObj) );
175}
176
189{
190 assert( !Hop_IsComplement(pObj) );
191 if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
192 return;
193 Hop_ConeMark_rec( Hop_ObjFanin0(pObj) );
194 Hop_ConeMark_rec( Hop_ObjFanin1(pObj) );
195 assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
196 Hop_ObjSetMarkA( pObj );
197}
198
211{
212 assert( !Hop_IsComplement(pObj) );
213 if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
214 return;
215 Hop_ConeCleanAndMark_rec( Hop_ObjFanin0(pObj) );
216 Hop_ConeCleanAndMark_rec( Hop_ObjFanin1(pObj) );
217 assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
218 Hop_ObjSetMarkA( pObj );
219 pObj->pData = NULL;
220}
221
234{
235 int Counter;
236 assert( !Hop_IsComplement(pObj) );
237 if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
238 return 0;
239 Counter = 1 + Hop_ConeCountAndMark_rec( Hop_ObjFanin0(pObj) ) +
240 Hop_ConeCountAndMark_rec( Hop_ObjFanin1(pObj) );
241 assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
242 Hop_ObjSetMarkA( pObj );
243 return Counter;
244}
245
258{
259 assert( !Hop_IsComplement(pObj) );
260 if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
261 return;
262 Hop_ConeUnmark_rec( Hop_ObjFanin0(pObj) );
263 Hop_ConeUnmark_rec( Hop_ObjFanin1(pObj) );
264 assert( Hop_ObjIsMarkA(pObj) ); // loop detection
265 Hop_ObjClearMarkA( pObj );
266}
267
280{
281 int Counter;
282 Counter = Hop_ConeCountAndMark_rec( Hop_Regular(pObj) );
283 Hop_ConeUnmark_rec( Hop_Regular(pObj) );
284 return Counter;
285}
286
299{
300 int Counter;
301 assert( !Hop_IsComplement(pObj) );
302 if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
303 return (int)(pObj == pPivot);
304 Counter = Hop_ObjFanoutCount_rec( Hop_ObjFanin0(pObj), pPivot ) +
305 Hop_ObjFanoutCount_rec( Hop_ObjFanin1(pObj), pPivot );
306 assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
307 Hop_ObjSetMarkA( pObj );
308 return Counter;
309}
311{
312 int Counter;
313 assert( !Hop_IsComplement(pPivot) );
314 Counter = Hop_ObjFanoutCount_rec( Hop_Regular(pObj), pPivot );
315 Hop_ConeUnmark_rec( Hop_Regular(pObj) );
316 return Counter;
317}
318
330void Hop_Transfer_rec( Hop_Man_t * pDest, Hop_Obj_t * pObj )
331{
332 assert( !Hop_IsComplement(pObj) );
333 if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
334 return;
335 Hop_Transfer_rec( pDest, Hop_ObjFanin0(pObj) );
336 Hop_Transfer_rec( pDest, Hop_ObjFanin1(pObj) );
337 pObj->pData = Hop_And( pDest, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) );
338 assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
339 Hop_ObjSetMarkA( pObj );
340}
341
353Hop_Obj_t * Hop_Transfer( Hop_Man_t * pSour, Hop_Man_t * pDest, Hop_Obj_t * pRoot, int nVars )
354{
355 Hop_Obj_t * pObj;
356 int i;
357 // solve simple cases
358 if ( pSour == pDest )
359 return pRoot;
360 if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
361 return Hop_NotCond( Hop_ManConst1(pDest), Hop_IsComplement(pRoot) );
362 // set the PI mapping
363 Hop_ManForEachPi( pSour, pObj, i )
364 {
365 if ( i == nVars )
366 break;
367 pObj->pData = Hop_IthVar(pDest, i);
368 }
369 // transfer and set markings
370 Hop_Transfer_rec( pDest, Hop_Regular(pRoot) );
371 // clear the markings
372 Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
373 return Hop_NotCond( (Hop_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
374}
375
387void Hop_Compose_rec( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pFunc, Hop_Obj_t * pVar )
388{
389 assert( !Hop_IsComplement(pObj) );
390 if ( Hop_ObjIsMarkA(pObj) )
391 return;
392 if ( Hop_ObjIsConst1(pObj) || Hop_ObjIsPi(pObj) )
393 {
394 pObj->pData = pObj == pVar ? pFunc : pObj;
395 return;
396 }
397 Hop_Compose_rec( p, Hop_ObjFanin0(pObj), pFunc, pVar );
398 Hop_Compose_rec( p, Hop_ObjFanin1(pObj), pFunc, pVar );
399 pObj->pData = Hop_And( p, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) );
400 assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
401 Hop_ObjSetMarkA( pObj );
402}
403
415Hop_Obj_t * Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, int iVar )
416{
417 // quit if the PI variable is not defined
418 if ( iVar >= Hop_ManPiNum(p) )
419 {
420 printf( "Hop_Compose(): The PI variable %d is not defined.\n", iVar );
421 return NULL;
422 }
423 // recursively perform composition
424 Hop_Compose_rec( p, Hop_Regular(pRoot), pFunc, Hop_ManPi(p, iVar) );
425 // clear the markings
426 Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
427 return Hop_NotCond( (Hop_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
428}
429
442{
443 assert( !Hop_IsComplement(pObj) );
444 if ( Hop_ObjIsMarkA(pObj) )
445 return;
446 if ( Hop_ObjIsConst1(pObj) || Hop_ObjIsPi(pObj) )
447 {
448 pObj->pData = pObj == pVar ? Hop_Not(pObj) : pObj;
449 return;
450 }
451 Hop_Complement_rec( p, Hop_ObjFanin0(pObj), pVar );
452 Hop_Complement_rec( p, Hop_ObjFanin1(pObj), pVar );
453 pObj->pData = Hop_And( p, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) );
454 assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
455 Hop_ObjSetMarkA( pObj );
456}
457
470{
471 // quit if the PI variable is not defined
472 if ( iVar >= Hop_ManPiNum(p) )
473 {
474 printf( "Hop_Complement(): The PI variable %d is not defined.\n", iVar );
475 return NULL;
476 }
477 // recursively perform composition
478 Hop_Complement_rec( p, Hop_Regular(pRoot), Hop_ManPi(p, iVar) );
479 // clear the markings
480 Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
481 return Hop_NotCond( (Hop_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
482}
483
496{
497 assert( !Hop_IsComplement(pObj) );
498 if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
499 return;
500 Hop_Remap_rec( p, Hop_ObjFanin0(pObj) );
501 Hop_Remap_rec( p, Hop_ObjFanin1(pObj) );
502 pObj->pData = Hop_And( p, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) );
503 assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
504 Hop_ObjSetMarkA( pObj );
505}
506
518Hop_Obj_t * Hop_Remap( Hop_Man_t * p, Hop_Obj_t * pRoot, unsigned uSupp, int nVars )
519{
520 Hop_Obj_t * pObj;
521 int i, k;
522 // quit if the PI variable is not defined
523 if ( nVars > Hop_ManPiNum(p) )
524 {
525 printf( "Hop_Remap(): The number of variables (%d) is more than the manager size (%d).\n", nVars, Hop_ManPiNum(p) );
526 return NULL;
527 }
528 // return if constant
529 if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
530 return pRoot;
531 if ( uSupp == 0 )
532 return Hop_NotCond( Hop_ManConst0(p), Hop_ObjPhaseCompl(pRoot) );
533 // set the PI mapping
534 k = 0;
535 Hop_ManForEachPi( p, pObj, i )
536 {
537 if ( i == nVars )
538 break;
539 if ( uSupp & (1 << i) )
540 pObj->pData = Hop_IthVar(p, k++);
541 else
542 pObj->pData = Hop_ManConst0(p);
543 }
544 assert( k > 0 && k < nVars );
545 // recursively perform composition
546 Hop_Remap_rec( p, Hop_Regular(pRoot) );
547 // clear the markings
548 Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
549 return Hop_NotCond( (Hop_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
550}
551
563Hop_Obj_t * Hop_Permute( Hop_Man_t * p, Hop_Obj_t * pRoot, int nRootVars, int * pPermute )
564{
565 Hop_Obj_t * pObj;
566 int i;
567 // return if constant
568 if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
569 return pRoot;
570 // create mapping
571 Hop_ManForEachPi( p, pObj, i )
572 {
573 if ( i == nRootVars )
574 break;
575 assert( pPermute[i] >= 0 && pPermute[i] < Hop_ManPiNum(p) );
576 pObj->pData = Hop_IthVar( p, pPermute[i] );
577 }
578 // recursively perform composition
579 Hop_Remap_rec( p, Hop_Regular(pRoot) );
580 // clear the markings
581 Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
582 return Hop_NotCond( (Hop_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
583}
584
588
589
591
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Cube * p
Definition exorList.c:222
void Hop_ConeUnmark_rec(Hop_Obj_t *pObj)
Definition hopDfs.c:257
Hop_Obj_t * Hop_Complement(Hop_Man_t *p, Hop_Obj_t *pRoot, int iVar)
Definition hopDfs.c:469
Hop_Obj_t * Hop_Compose(Hop_Man_t *p, Hop_Obj_t *pRoot, Hop_Obj_t *pFunc, int iVar)
Definition hopDfs.c:415
ABC_NAMESPACE_IMPL_START void Hop_ManDfs_rec(Hop_Obj_t *pObj, Vec_Ptr_t *vNodes)
DECLARATIONS ///.
Definition hopDfs.c:45
Hop_Obj_t * Hop_Permute(Hop_Man_t *p, Hop_Obj_t *pRoot, int nRootVars, int *pPermute)
Definition hopDfs.c:563
Hop_Obj_t * Hop_Remap(Hop_Man_t *p, Hop_Obj_t *pRoot, unsigned uSupp, int nVars)
Definition hopDfs.c:518
Vec_Ptr_t * Hop_ManDfs(Hop_Man_t *p)
Definition hopDfs.c:68
Vec_Ptr_t * Hop_ManDfsNode(Hop_Man_t *p, Hop_Obj_t *pNode)
Definition hopDfs.c:92
int Hop_ManCountLevels(Hop_Man_t *p)
Definition hopDfs.c:116
void Hop_Transfer_rec(Hop_Man_t *pDest, Hop_Obj_t *pObj)
Definition hopDfs.c:330
void Hop_Remap_rec(Hop_Man_t *p, Hop_Obj_t *pObj)
Definition hopDfs.c:495
int Hop_ObjFanoutCount(Hop_Obj_t *pObj, Hop_Obj_t *pPivot)
Definition hopDfs.c:310
void Hop_Compose_rec(Hop_Man_t *p, Hop_Obj_t *pObj, Hop_Obj_t *pFunc, Hop_Obj_t *pVar)
Definition hopDfs.c:387
int Hop_DagSize(Hop_Obj_t *pObj)
Definition hopDfs.c:279
int Hop_ObjFanoutCount_rec(Hop_Obj_t *pObj, Hop_Obj_t *pPivot)
Definition hopDfs.c:298
Hop_Obj_t * Hop_Transfer(Hop_Man_t *pSour, Hop_Man_t *pDest, Hop_Obj_t *pRoot, int nVars)
Definition hopDfs.c:353
void Hop_ConeCleanAndMark_rec(Hop_Obj_t *pObj)
Definition hopDfs.c:210
void Hop_ConeMark_rec(Hop_Obj_t *pObj)
Definition hopDfs.c:188
int Hop_ConeCountAndMark_rec(Hop_Obj_t *pObj)
Definition hopDfs.c:233
void Hop_Complement_rec(Hop_Man_t *p, Hop_Obj_t *pObj, Hop_Obj_t *pVar)
Definition hopDfs.c:441
void Hop_ManCreateRefs(Hop_Man_t *p)
Definition hopDfs.c:152
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition hop.h:49
Hop_Obj_t * Hop_IthVar(Hop_Man_t *p, int i)
FUNCTION DEFINITIONS ///.
Definition hopOper.c:63
#define Hop_ManForEachPi(p, pObj, i)
ITERATORS ///.
Definition hop.h:259
#define Hop_ManForEachNode(p, pObj, i)
Definition hop.h:265
Hop_Obj_t * Hop_And(Hop_Man_t *p, Hop_Obj_t *p0, Hop_Obj_t *p1)
Definition hopOper.c:104
#define Hop_ManForEachPo(p, pObj, i)
Definition hop.h:262
struct Hop_Obj_t_ Hop_Obj_t
Definition hop.h:50
void * pData
Definition hop.h:68
#define assert(ex)
Definition util_old.h:213
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