ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
aigRepr.c
Go to the documentation of this file.
1
20
21#include "aig.h"
22
24
25
29
33
45void Aig_ManReprStart( Aig_Man_t * p, int nIdMax )
46{
47 assert( Aig_ManBufNum(p) == 0 );
48 assert( p->pReprs == NULL );
49 p->nReprsAlloc = nIdMax;
50 p->pReprs = ABC_ALLOC( Aig_Obj_t *, p->nReprsAlloc );
51 memset( p->pReprs, 0, sizeof(Aig_Obj_t *) * p->nReprsAlloc );
52}
53
66{
67 assert( p->pReprs != NULL );
68 ABC_FREE( p->pReprs );
69 p->nReprsAlloc = 0;
70}
71
83void Aig_ObjCreateRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 )
84{
85 assert( p->pReprs != NULL );
86 assert( !Aig_IsComplement(pNode1) );
87 assert( !Aig_IsComplement(pNode2) );
88 assert( pNode1->Id < p->nReprsAlloc );
89 assert( pNode2->Id < p->nReprsAlloc );
90 assert( pNode1->Id < pNode2->Id );
91 p->pReprs[pNode2->Id] = pNode1;
92}
93
105static inline void Aig_ObjSetRepr_( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 )
106{
107 assert( p->pReprs != NULL );
108 assert( !Aig_IsComplement(pNode1) );
109 assert( !Aig_IsComplement(pNode2) );
110 assert( pNode1->Id < p->nReprsAlloc );
111 assert( pNode2->Id < p->nReprsAlloc );
112 if ( pNode1 == pNode2 )
113 return;
114 if ( pNode1->Id < pNode2->Id )
115 p->pReprs[pNode2->Id] = pNode1;
116 else
117 p->pReprs[pNode1->Id] = pNode2;
118}
119
131static inline Aig_Obj_t * Aig_ObjFindRepr( Aig_Man_t * p, Aig_Obj_t * pNode )
132{
133 assert( p->pReprs != NULL );
134 assert( !Aig_IsComplement(pNode) );
135 assert( pNode->Id < p->nReprsAlloc );
136// assert( !p->pReprs[pNode->Id] || p->pReprs[pNode->Id]->Id < pNode->Id );
137 return p->pReprs[pNode->Id];
138}
139
151static inline void Aig_ObjClearRepr( Aig_Man_t * p, Aig_Obj_t * pNode )
152{
153 assert( p->pReprs != NULL );
154 assert( !Aig_IsComplement(pNode) );
155 assert( pNode->Id < p->nReprsAlloc );
156 p->pReprs[pNode->Id] = NULL;
157}
158
170static inline Aig_Obj_t * Aig_ObjFindReprTransitive( Aig_Man_t * p, Aig_Obj_t * pNode )
171{
172 Aig_Obj_t * pNext, * pRepr;
173 if ( (pRepr = Aig_ObjFindRepr(p, pNode)) )
174 while ( (pNext = Aig_ObjFindRepr(p, pRepr)) )
175 pRepr = pNext;
176 return pRepr;
177}
178
190static inline Aig_Obj_t * Aig_ObjGetRepr( Aig_Man_t * p, Aig_Obj_t * pObj )
191{
192 Aig_Obj_t * pRepr;
193 if ( (pRepr = Aig_ObjFindRepr(p, pObj)) )
194 return Aig_NotCond( (Aig_Obj_t *)pRepr->pData, pObj->fPhase ^ pRepr->fPhase );
195 return (Aig_Obj_t *)pObj->pData;
196}
197static inline Aig_Obj_t * Aig_ObjChild0Repr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjGetRepr(p, Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) ); }
198static inline Aig_Obj_t * Aig_ObjChild1Repr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjGetRepr(p, Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) ); }
199
212{
213 Aig_Obj_t * pObj, * pRepr;
214 int k;
215 assert( pNew->pReprs != NULL );
216 // extend storage to fix pNew
217 if ( pNew->nReprsAlloc < Aig_ManObjNumMax(pNew) )
218 {
219 int nReprsAllocNew = 2 * Aig_ManObjNumMax(pNew);
220 pNew->pReprs = ABC_REALLOC( Aig_Obj_t *, pNew->pReprs, nReprsAllocNew );
221 memset( pNew->pReprs + pNew->nReprsAlloc, 0, sizeof(Aig_Obj_t *) * (nReprsAllocNew-pNew->nReprsAlloc) );
222 pNew->nReprsAlloc = nReprsAllocNew;
223 }
224 // go through the nodes which have representatives
225 Aig_ManForEachObj( pOld, pObj, k )
226 if ( (pRepr = Aig_ObjFindRepr(pOld, pObj)) )
227 Aig_ObjSetRepr_( pNew, Aig_Regular((Aig_Obj_t *)pRepr->pData), Aig_Regular((Aig_Obj_t *)pObj->pData) );
228}
229
242{
243 Aig_Obj_t * pRepr;
244 if ( pObj->pData )
245 return (Aig_Obj_t *)pObj->pData;
246 if ( (pRepr = Aig_ObjFindRepr(p, pObj)) )
247 {
248 Aig_ManDupRepr_rec( pNew, p, pRepr );
249 return (Aig_Obj_t *)(pObj->pData = Aig_NotCond( (Aig_Obj_t *)pRepr->pData, pRepr->fPhase ^ pObj->fPhase ));
250 }
251 Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin0(pObj) );
252 Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin1(pObj) );
253 return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) ));
254}
255
268{
269 Aig_Man_t * pNew;
270 Aig_Obj_t * pObj;
271 int i;
272 // start the HOP package
273 pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
274 pNew->pName = Abc_UtilStrsav( p->pName );
275 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
276 pNew->nConstrs = p->nConstrs;
277 pNew->nBarBufs = p->nBarBufs;
278 if ( p->vFlopNums )
279 pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
280 // map the const and primary inputs
282 Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
283 Aig_ManForEachCi( p, pObj, i )
284 pObj->pData = Aig_ObjCreateCi(pNew);
285// Aig_ManForEachCi( p, pObj, i )
286// pObj->pData = Aig_ObjGetRepr( p, pObj );
287 // map the internal nodes
288 if ( fOrdered )
289 {
290 Aig_ManForEachNode( p, pObj, i )
291 pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) );
292 }
293 else
294 {
295// Aig_ManForEachObj( p, pObj, i )
296// if ( p->pReprs[i] )
297// printf( "Substituting %d for %d.\n", p->pReprs[i]->Id, pObj->Id );
298
299 Aig_ManForEachCo( p, pObj, i )
300 Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin0(pObj) );
301 }
302 // transfer the POs
303 Aig_ManForEachCo( p, pObj, i )
304 Aig_ObjCreateCo( pNew, Aig_ObjChild0Repr(p, pObj) );
305 Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
306 // check the new manager
307 if ( !Aig_ManCheck(pNew) )
308 printf( "Aig_ManDupRepr: Check has failed.\n" );
309 return pNew;
310}
311
324{
325 Aig_Man_t * pNew;
326 Aig_Obj_t * pObj;
327 int i;
328 assert( p->pReprs != NULL );
329 // reconstruct AIG with representatives
330 pNew = Aig_ManDupRepr( p, 0 );
331 // perfrom sequential cleanup but do not remove registers
333 // remove pointers to the dead nodes
334 Aig_ManForEachObj( p, pObj, i )
335 if ( pObj->pData && Aig_ObjIsNone((Aig_Obj_t *)pObj->pData) )
336 pObj->pData = NULL;
337 return pNew;
338}
339
352{
353 Aig_Obj_t * pObj, * pRepr;
354 int i, nFanouts = 0;
355 Aig_ManForEachNode( p, pObj, i )
356 {
357 pRepr = Aig_ObjFindReprTransitive( p, pObj );
358 if ( pRepr == NULL )
359 continue;
360 assert( pRepr->Id < pObj->Id );
361 Aig_ObjSetRepr_( p, pObj, pRepr );
362 nFanouts += (pObj->nRefs > 0);
363 }
364 return nFanouts;
365}
366
379{
380 Aig_Obj_t * pObj;
381 int i, Counter = 0;
382 if ( p->pReprs == NULL )
383 return 0;
384 Aig_ManForEachObj( p, pObj, i )
385 Counter += (p->pReprs[i] != NULL);
386 return Counter;
387}
388
401{
402 // check the trivial cases
403 if ( pNode == NULL )
404 return 0;
405 if ( Aig_ObjIsCi(pNode) )
406 return 0;
407// if ( pNode->Id < pOld->Id ) // cannot use because of choices of pNode
408// return 0;
409 if ( pNode == pOld )
410 return 1;
411 // skip the visited node
412 if ( Aig_ObjIsTravIdCurrent( p, pNode ) )
413 return 0;
414 Aig_ObjSetTravIdCurrent( p, pNode );
415 // check the children
416 if ( Aig_ObjCheckTfi_rec( p, Aig_ObjFanin0(pNode), pOld ) )
417 return 1;
418 if ( Aig_ObjCheckTfi_rec( p, Aig_ObjFanin1(pNode), pOld ) )
419 return 1;
420 // check equivalent nodes
421 return Aig_ObjCheckTfi_rec( p, Aig_ObjEquiv(p, pNode), pOld );
422}
423
436{
437 assert( !Aig_IsComplement(pNew) );
438 assert( !Aig_IsComplement(pOld) );
440 return Aig_ObjCheckTfi_rec( p, pNew, pOld );
441}
442
455{
456 Aig_Man_t * pTemp;
457 int i, nFanouts;
458 assert( p->pReprs != NULL );
459 for ( i = 0; (nFanouts = Aig_ManRemapRepr( p )); i++ )
460 {
461// printf( "Iter = %3d. Fanouts = %6d. Nodes = %7d.\n", i+1, nFanouts, Aig_ManNodeNum(p) );
462 p = Aig_ManDupRepr( pTemp = p, 1 );
463 Aig_ManReprStart( p, Aig_ManObjNumMax(p) );
464 Aig_ManTransferRepr( p, pTemp );
465 Aig_ManStop( pTemp );
466 }
467 return p;
468}
469
482{
483 Aig_Obj_t * pObj, * pRepr;
484 int i;
485 assert( p->pReprs != NULL );
486 // create equivalent nodes in the manager
487 assert( p->pEquivs == NULL );
488 p->pEquivs = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
489 memset( p->pEquivs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
490 // make the choice nodes
491 Aig_ManForEachNode( p, pObj, i )
492 {
493 pRepr = Aig_ObjFindRepr( p, pObj );
494 if ( pRepr == NULL )
495 continue;
496 // skip constant and PI classes
497 if ( !Aig_ObjIsNode(pRepr) )
498 {
499 Aig_ObjClearRepr( p, pObj );
500 continue;
501 }
502 // skip choices with combinatinal loops
503 if ( Aig_ObjCheckTfi( p, pObj, pRepr ) )
504 {
505 Aig_ObjClearRepr( p, pObj );
506 continue;
507 }
508//printf( "Node %d is represented by node %d.\n", pObj->Id, pRepr->Id );
509 // add choice to the choice node
510 if ( pObj->nRefs > 0 )
511 {
512 Aig_ObjClearRepr( p, pObj );
513 continue;
514 }
515 assert( pObj->nRefs == 0 );
516 p->pEquivs[pObj->Id] = p->pEquivs[pRepr->Id];
517 p->pEquivs[pRepr->Id] = pObj;
518 }
519}
520
521
533int Aig_TransferMappedClasses( Aig_Man_t * pAig, Aig_Man_t * pPart, int * pMapBack )
534{
535 Aig_Obj_t * pObj;
536 int nClasses, k;
537 nClasses = 0;
538 if ( pPart->pReprs ) {
539 Aig_ManForEachObj( pPart, pObj, k )
540 {
541 if ( pPart->pReprs[pObj->Id] == NULL )
542 continue;
543 nClasses++;
544 Aig_ObjSetRepr_( pAig,
545 Aig_ManObj(pAig, pMapBack[pObj->Id]),
546 Aig_ManObj(pAig, pMapBack[pPart->pReprs[pObj->Id]->Id]) );
547 }
548 }
549 return nClasses;
550}
551
552
556
557
559
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_REALLOC(type, obj, num)
Definition abc_global.h:268
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Aig_Obj_t * Aig_ManDupRepr_rec(Aig_Man_t *pNew, Aig_Man_t *p, Aig_Obj_t *pObj)
Definition aigRepr.c:241
Aig_Man_t * Aig_ManDupRepr(Aig_Man_t *p, int fOrdered)
Definition aigRepr.c:267
Aig_Man_t * Aig_ManRehash(Aig_Man_t *p)
Definition aigRepr.c:454
void Aig_ManTransferRepr(Aig_Man_t *pNew, Aig_Man_t *pOld)
Definition aigRepr.c:211
int Aig_ObjCheckTfi(Aig_Man_t *p, Aig_Obj_t *pNew, Aig_Obj_t *pOld)
Definition aigRepr.c:435
void Aig_ObjCreateRepr(Aig_Man_t *p, Aig_Obj_t *pNode1, Aig_Obj_t *pNode2)
Definition aigRepr.c:83
int Aig_ManRemapRepr(Aig_Man_t *p)
Definition aigRepr.c:351
int Aig_ObjCheckTfi_rec(Aig_Man_t *p, Aig_Obj_t *pNode, Aig_Obj_t *pOld)
Definition aigRepr.c:400
ABC_NAMESPACE_IMPL_START void Aig_ManReprStart(Aig_Man_t *p, int nIdMax)
DECLARATIONS ///.
Definition aigRepr.c:45
void Aig_ManMarkValidChoices(Aig_Man_t *p)
Definition aigRepr.c:481
void Aig_ManReprStop(Aig_Man_t *p)
Definition aigRepr.c:65
int Aig_ManCountReprs(Aig_Man_t *p)
Definition aigRepr.c:378
int Aig_TransferMappedClasses(Aig_Man_t *pAig, Aig_Man_t *pPart, int *pMapBack)
Definition aigRepr.c:533
Aig_Man_t * Aig_ManDupReprBasic(Aig_Man_t *p)
Definition aigRepr.c:323
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition aigMan.c:438
#define Aig_ManForEachObj(p, pObj, i)
Definition aig.h:403
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
int Aig_ManSeqCleanupBasic(Aig_Man_t *p)
Definition aigScl.c:257
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigUtil.c:44
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:104
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition aigObj.c:66
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition aigMan.c:47
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigObj.c:45
void Aig_ManCleanData(Aig_Man_t *p)
Definition aigUtil.c:205
ABC_DLL int Aig_ManCheck(Aig_Man_t *p)
FUNCTION DECLARATIONS ///.
Definition aigCheck.c:45
Cube * p
Definition exorList.c:222
int Id
Definition aig.h:85
unsigned int nRefs
Definition aig.h:81
void * pData
Definition aig.h:87
unsigned int fPhase
Definition aig.h:78
#define assert(ex)
Definition util_old.h:213
char * memset()