ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
aigOper.c
Go to the documentation of this file.
1
20
21#include "aig.h"
22
24
25
29
30// procedure to detect an EXOR gate
31static inline int Aig_ObjIsExorType( Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 )
32{
33 if ( !Aig_IsComplement(p0) || !Aig_IsComplement(p1) )
34 return 0;
35 p0 = Aig_Regular(p0);
36 p1 = Aig_Regular(p1);
37 if ( !Aig_ObjIsAnd(p0) || !Aig_ObjIsAnd(p1) )
38 return 0;
39 if ( Aig_ObjFanin0(p0) != Aig_ObjFanin0(p1) || Aig_ObjFanin1(p0) != Aig_ObjFanin1(p1) )
40 return 0;
41 if ( Aig_ObjFaninC0(p0) == Aig_ObjFaninC0(p1) || Aig_ObjFaninC1(p0) == Aig_ObjFaninC1(p1) )
42 return 0;
43 *ppFan0 = Aig_ObjChild0(p0);
44 *ppFan1 = Aig_ObjChild1(p0);
45 return 1;
46}
47
51
64{
65 int v;
66 for ( v = Aig_ManCiNum(p); v <= i; v++ )
68 assert( i < Vec_PtrSize(p->vCis) );
69 return Aig_ManCi( p, i );
70}
71
84{
85 if ( Type == AIG_OBJ_AND )
86 return Aig_And( p, p0, p1 );
87 if ( Type == AIG_OBJ_EXOR )
88 return Aig_Exor( p, p0, p1 );
89 assert( 0 );
90 return NULL;
91}
92
105{
106 Aig_Obj_t * pGhost, * pResult;
107 Aig_Obj_t * pFan0, * pFan1;
108 // check trivial cases
109 if ( p0 == p1 )
110 return p0;
111 if ( p0 == Aig_Not(p1) )
112 return Aig_Not(p->pConst1);
113 if ( Aig_Regular(p0) == p->pConst1 )
114 return p0 == p->pConst1 ? p1 : Aig_Not(p->pConst1);
115 if ( Aig_Regular(p1) == p->pConst1 )
116 return p1 == p->pConst1 ? p0 : Aig_Not(p->pConst1);
117 // check not so trivial cases
118 if ( p->fAddStrash && (Aig_ObjIsNode(Aig_Regular(p0)) || Aig_ObjIsNode(Aig_Regular(p1))) )
119 { // http://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf
120 Aig_Obj_t * pFanA, * pFanB, * pFanC, * pFanD;
121 pFanA = Aig_ObjChild0(Aig_Regular(p0));
122 pFanB = Aig_ObjChild1(Aig_Regular(p0));
123 pFanC = Aig_ObjChild0(Aig_Regular(p1));
124 pFanD = Aig_ObjChild1(Aig_Regular(p1));
125 if ( Aig_IsComplement(p0) )
126 {
127 if ( pFanA == Aig_Not(p1) || pFanB == Aig_Not(p1) )
128 return p1;
129 if ( pFanB == p1 )
130 return Aig_And( p, Aig_Not(pFanA), pFanB );
131 if ( pFanA == p1 )
132 return Aig_And( p, Aig_Not(pFanB), pFanA );
133 }
134 else
135 {
136 if ( pFanA == Aig_Not(p1) || pFanB == Aig_Not(p1) )
137 return Aig_Not(p->pConst1);
138 if ( pFanA == p1 || pFanB == p1 )
139 return p0;
140 }
141 if ( Aig_IsComplement(p1) )
142 {
143 if ( pFanC == Aig_Not(p0) || pFanD == Aig_Not(p0) )
144 return p0;
145 if ( pFanD == p0 )
146 return Aig_And( p, Aig_Not(pFanC), pFanD );
147 if ( pFanC == p0 )
148 return Aig_And( p, Aig_Not(pFanD), pFanC );
149 }
150 else
151 {
152 if ( pFanC == Aig_Not(p0) || pFanD == Aig_Not(p0) )
153 return Aig_Not(p->pConst1);
154 if ( pFanC == p0 || pFanD == p0 )
155 return p1;
156 }
157 if ( !Aig_IsComplement(p0) && !Aig_IsComplement(p1) )
158 {
159 if ( pFanA == Aig_Not(pFanC) || pFanA == Aig_Not(pFanD) || pFanB == Aig_Not(pFanC) || pFanB == Aig_Not(pFanD) )
160 return Aig_Not(p->pConst1);
161 if ( pFanA == pFanC || pFanB == pFanC )
162 return Aig_And( p, p0, pFanD );
163 if ( pFanB == pFanC || pFanB == pFanD )
164 return Aig_And( p, pFanA, p1 );
165 if ( pFanA == pFanD || pFanB == pFanD )
166 return Aig_And( p, p0, pFanC );
167 if ( pFanA == pFanC || pFanA == pFanD )
168 return Aig_And( p, pFanB, p1 );
169 }
170 else if ( Aig_IsComplement(p0) && !Aig_IsComplement(p1) )
171 {
172 if ( pFanA == Aig_Not(pFanC) || pFanA == Aig_Not(pFanD) || pFanB == Aig_Not(pFanC) || pFanB == Aig_Not(pFanD) )
173 return p1;
174 if ( pFanB == pFanC || pFanB == pFanD )
175 return Aig_And( p, Aig_Not(pFanA), p1 );
176 if ( pFanA == pFanC || pFanA == pFanD )
177 return Aig_And( p, Aig_Not(pFanB), p1 );
178 }
179 else if ( !Aig_IsComplement(p0) && Aig_IsComplement(p1) )
180 {
181 if ( pFanC == Aig_Not(pFanA) || pFanC == Aig_Not(pFanB) || pFanD == Aig_Not(pFanA) || pFanD == Aig_Not(pFanB) )
182 return p0;
183 if ( pFanD == pFanA || pFanD == pFanB )
184 return Aig_And( p, Aig_Not(pFanC), p0 );
185 if ( pFanC == pFanA || pFanC == pFanB )
186 return Aig_And( p, Aig_Not(pFanD), p0 );
187 }
188 else // if ( Aig_IsComplement(p0) && Aig_IsComplement(p1) )
189 {
190 if ( pFanA == pFanD && pFanB == Aig_Not(pFanC) )
191 return Aig_Not(pFanA);
192 if ( pFanB == pFanC && pFanA == Aig_Not(pFanD) )
193 return Aig_Not(pFanB);
194 if ( pFanA == pFanC && pFanB == Aig_Not(pFanD) )
195 return Aig_Not(pFanA);
196 if ( pFanB == pFanD && pFanA == Aig_Not(pFanC) )
197 return Aig_Not(pFanB);
198 }
199 }
200 // check if it can be an EXOR gate
201 if ( p->fCatchExor && Aig_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
202 return Aig_Exor( p, pFan0, pFan1 );
203 pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_AND );
204 if ( (pResult = Aig_TableLookup( p, pGhost )) )
205 return pResult;
206 return Aig_ObjCreate( p, pGhost );
207}
208
221{
222 Aig_Obj_t * pGhost, * pResult;
223 int fCompl;
224 // check trivial cases
225 if ( p0 == p1 )
226 return Aig_Not(p->pConst1);
227 if ( p0 == Aig_Not(p1) )
228 return p->pConst1;
229 if ( Aig_Regular(p0) == p->pConst1 )
230 return Aig_NotCond( p1, p0 == p->pConst1 );
231 if ( Aig_Regular(p1) == p->pConst1 )
232 return Aig_NotCond( p0, p1 == p->pConst1 );
233 // when there is no special XOR gates
234 if ( !p->fCatchExor )
235 return Aig_Or( p, Aig_And(p, p0, Aig_Not(p1)), Aig_And(p, Aig_Not(p0), p1) );
236 // canonicize
237 fCompl = Aig_IsComplement(p0) ^ Aig_IsComplement(p1);
238 p0 = Aig_Regular(p0);
239 p1 = Aig_Regular(p1);
240 pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_EXOR );
241 // check the table
242 if ( (pResult = Aig_TableLookup( p, pGhost )) )
243 return Aig_NotCond( pResult, fCompl );
244 pResult = Aig_ObjCreate( p, pGhost );
245 return Aig_NotCond( pResult, fCompl );
246}
247
260{
261 return Aig_Not( Aig_And( p, Aig_Not(p0), Aig_Not(p1) ) );
262}
263
276{
277 if ( p0 == p1 )
278 return p0;
279 if ( p0 == Aig_ManConst0(p) || p1 == Aig_ManConst0(p) || p0 == Aig_Not(p1) )
280 return Aig_ManConst0(p);
281 if ( p0 == Aig_ManConst1(p) )
282 return p1;
283 if ( p1 == Aig_ManConst1(p) )
284 return p0;
285 if ( Aig_Regular(p0)->Id < Aig_Regular(p1)->Id )
286 return Aig_TableLookup( p, Aig_ObjCreateGhost(p, p0, p1, AIG_OBJ_AND) );
287 return Aig_TableLookup( p, Aig_ObjCreateGhost(p, p1, p0, AIG_OBJ_AND) );
288}
289
302{
303 return Aig_Or( p, Aig_And(p, pC, p1), Aig_And(p, Aig_Not(pC), p0) );
304}
305
318{
319 int fUseMuxCanon = 0;
320 Aig_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp;
321 int Count0, Count1;
322 if ( !fUseMuxCanon )
323 return Aig_Mux2( p, pC, p1, p0 );
324 if ( p0 == p1 )
325 return p0;
326 if ( p1 == Aig_Not(p0) )
327 return Aig_Exor( p, pC, p0 );
328 if ( pC == Aig_ManConst0(p) )
329 return p0;
330 if ( pC == Aig_ManConst1(p) )
331 return p1;
332 if ( p0 == Aig_ManConst0(p) )
333 return Aig_And( p, pC, p1 );
334 if ( p0 == Aig_ManConst1(p) )
335 return Aig_Or( p, Aig_Not(pC), p1 );
336 if ( p1 == Aig_ManConst0(p) )
337 return Aig_And( p, Aig_Not(pC), p0 );
338 if ( p1 == Aig_ManConst1(p) )
339 return Aig_Or( p, pC, p0 );
340 // implement the first MUX (F = C * x1 + C' * x0)
341 pTempA1 = Aig_TableLookupInt( p, pC, p1 );
342 pTempA2 = Aig_TableLookupInt( p, Aig_Not(pC), p0 );
343 if ( pTempA1 && pTempA2 )
344 {
345 pTemp = Aig_TableLookupInt( p, Aig_Not(pTempA1), Aig_Not(pTempA2) );
346 if ( pTemp ) return Aig_Not(pTemp);
347 }
348 Count0 = (pTempA1 != NULL) + (pTempA2 != NULL);
349 // implement the second MUX (F' = C * x1' + C' * x0')
350 pTempB1 = Aig_TableLookupInt( p, pC, Aig_Not(p1) );
351 pTempB2 = Aig_TableLookupInt( p, Aig_Not(pC), Aig_Not(p0) );
352 if ( pTempB1 && pTempB2 )
353 {
354 pTemp = Aig_TableLookupInt( p, Aig_Not(pTempB1), Aig_Not(pTempB2) );
355 if ( pTemp ) return pTemp;
356 }
357 Count1 = (pTempB1 != NULL) + (pTempB2 != NULL);
358 // compare and decide which one to implement
359 if ( Count0 >= Count1 )
360 return Aig_Or( p, Aig_And(p, pC, p1), Aig_And(p, Aig_Not(pC), p0) );
361 return Aig_Not( Aig_Or( p, Aig_And(p, pC, Aig_Not(p1)), Aig_And(p, Aig_Not(pC), Aig_Not(p0)) ) );
362// return Aig_Or( p, Aig_And(p, pC, p1), Aig_And(p, Aig_Not(pC), p0) );
363}
364
377{
378 return Aig_Or( p, Aig_Or(p, Aig_And(p, pA, pB), Aig_And(p, pA, pC)), Aig_And(p, pB, pC) );
379}
380
392Aig_Obj_t * Aig_Multi_rec( Aig_Man_t * p, Aig_Obj_t ** ppObjs, int nObjs, Aig_Type_t Type )
393{
394 Aig_Obj_t * pObj1, * pObj2;
395 if ( nObjs == 1 )
396 return ppObjs[0];
397 pObj1 = Aig_Multi_rec( p, ppObjs, nObjs/2, Type );
398 pObj2 = Aig_Multi_rec( p, ppObjs + nObjs/2, nObjs - nObjs/2, Type );
399 return Aig_Oper( p, pObj1, pObj2, Type );
400}
401
413Aig_Obj_t * Aig_Multi( Aig_Man_t * p, Aig_Obj_t ** pArgs, int nArgs, Aig_Type_t Type )
414{
415 assert( Type == AIG_OBJ_AND || Type == AIG_OBJ_EXOR );
416 assert( nArgs > 0 );
417 return Aig_Multi_rec( p, pArgs, nArgs, Type );
418}
419
432{
433 int i;
434 assert( vPairs->nSize > 0 );
435 assert( vPairs->nSize % 2 == 0 );
436 for ( i = 0; i < vPairs->nSize; i += 2 )
437 vPairs->pArray[i/2] = Aig_Not( Aig_Exor( p, (Aig_Obj_t *)vPairs->pArray[i], (Aig_Obj_t *)vPairs->pArray[i+1] ) );
438 vPairs->nSize = vPairs->nSize/2;
439 return Aig_Not( Aig_Multi_rec( p, (Aig_Obj_t **)vPairs->pArray, vPairs->nSize, AIG_OBJ_AND ) );
440}
441
454{
455 int i;
456 assert( vNodes1->nSize > 0 && vNodes2->nSize > 0 );
457 assert( vNodes1->nSize == vNodes2->nSize );
458 for ( i = 0; i < vNodes1->nSize; i++ )
459 vNodes1->pArray[i] = Aig_Not( Aig_Exor( p, (Aig_Obj_t *)vNodes1->pArray[i], (Aig_Obj_t *)vNodes2->pArray[i] ) );
460 return Aig_Not( Aig_Multi_rec( p, (Aig_Obj_t **)vNodes1->pArray, vNodes1->nSize, AIG_OBJ_AND ) );
461}
462
475{
476 Aig_Obj_t * pFunc;
477 int i;
478 pFunc = Aig_ManConst1( p );
479 for ( i = 0; i < nVars; i++ )
480 pFunc = Aig_And( p, pFunc, Aig_IthVar(p, i) );
481 return pFunc;
482}
483
496{
497 Aig_Obj_t * pFunc;
498 int i;
499 pFunc = Aig_ManConst0( p );
500 for ( i = 0; i < nVars; i++ )
501 pFunc = Aig_Or( p, pFunc, Aig_IthVar(p, i) );
502 return pFunc;
503}
504
517{
518 Aig_Obj_t * pFunc;
519 int i;
520 pFunc = Aig_ManConst0( p );
521 for ( i = 0; i < nVars; i++ )
522 pFunc = Aig_Exor( p, pFunc, Aig_IthVar(p, i) );
523 return pFunc;
524}
525
538{
539 Vec_Ptr_t * vNodes;
540 Aig_Man_t * p;
541 Aig_Obj_t * pObj, * pFanin0, * pFanin1, * pCtrl;
542 int nNodes = 2000;
543 int i,nPIs = 20;
544// srand( time(NULL) );
545 srand( 321 );
546 vNodes = Vec_PtrAlloc( 100 );
547 // create a bunch of random MUXes
548 p = Aig_ManStart( 10000 );
549 for ( i = 0; i < nPIs; i++ )
550 Aig_IthVar(p,i);
551 for ( i = 0; i < nNodes; i++ )
552 {
553 if ( rand() % 10 == 0 )
554 pCtrl = Aig_ManConst0(p);
555 else if ( rand() % 10 == 0 )
556 pCtrl = Aig_ManConst1(p);
557 else if ( rand() % 3 == 0 || i < nPIs )
558 pCtrl = Aig_IthVar( p, rand() % nPIs );
559 else
560 pCtrl = (Aig_Obj_t *)Vec_PtrEntry(vNodes, rand() % i);
561 if ( rand() % 2 == 0 )
562 pCtrl = Aig_Not( pCtrl );
563
564 if ( rand() % 10 == 0 )
565 pFanin1 = Aig_ManConst0(p);
566 else if ( rand() % 10 == 0 )
567 pFanin1 = Aig_ManConst1(p);
568 else if ( rand() % 3 == 0 || i < nPIs )
569 pFanin1 = Aig_IthVar( p, rand() % nPIs );
570 else
571 pFanin1 = (Aig_Obj_t *)Vec_PtrEntry(vNodes, rand() % i);
572 if ( rand() % 2 == 0 )
573 pFanin1 = Aig_Not( pFanin1 );
574
575 if ( rand() % 10 == 0 )
576 pFanin0 = Aig_ManConst0(p);
577 else if ( rand() % 10 == 0 )
578 pFanin0 = Aig_ManConst1(p);
579 else if ( rand() % 3 == 0 || i < nPIs )
580 pFanin0 = Aig_IthVar( p, rand() % nPIs );
581 else
582 pFanin0 = (Aig_Obj_t *)Vec_PtrEntry(vNodes, rand() % i);
583 if ( rand() % 2 == 0 )
584 pFanin0 = Aig_Not( pFanin0 );
585
586 pObj = Aig_Mux( p, pCtrl, pFanin1, pFanin0 );
587 Vec_PtrPush( vNodes, pObj );
588 }
589 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
590 Aig_ObjCreateCo( p, pObj );
591 Vec_PtrFree( vNodes );
592
593 printf( "Number of nodes = %6d.\n", Aig_ManObjNum(p) );
594 Aig_ManCleanup( p );
595 printf( "Number of nodes = %6d.\n", Aig_ManObjNum(p) );
596 Aig_ManDumpBlif( p, "test1.blif", NULL, NULL );
597 Aig_ManStop( p );
598}
599
603
604
606
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Aig_Obj_t * Aig_CreateAnd(Aig_Man_t *p, int nVars)
Definition aigOper.c:474
Aig_Obj_t * Aig_Maj(Aig_Man_t *p, Aig_Obj_t *pA, Aig_Obj_t *pB, Aig_Obj_t *pC)
Definition aigOper.c:376
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_Mux(Aig_Man_t *p, Aig_Obj_t *pC, Aig_Obj_t *p1, Aig_Obj_t *p0)
Definition aigOper.c:317
Aig_Obj_t * Aig_Oper(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1, Aig_Type_t Type)
Definition aigOper.c:83
Aig_Obj_t * Aig_Miter(Aig_Man_t *p, Vec_Ptr_t *vPairs)
Definition aigOper.c:431
Aig_Obj_t * Aig_Exor(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:220
Aig_Obj_t * Aig_Multi_rec(Aig_Man_t *p, Aig_Obj_t **ppObjs, int nObjs, Aig_Type_t Type)
Definition aigOper.c:392
Aig_Obj_t * Aig_CreateExor(Aig_Man_t *p, int nVars)
Definition aigOper.c:516
Aig_Obj_t * Aig_Mux2(Aig_Man_t *p, Aig_Obj_t *pC, Aig_Obj_t *p1, Aig_Obj_t *p0)
Definition aigOper.c:301
Aig_Obj_t * Aig_Multi(Aig_Man_t *p, Aig_Obj_t **pArgs, int nArgs, Aig_Type_t Type)
Definition aigOper.c:413
Aig_Obj_t * Aig_CreateOr(Aig_Man_t *p, int nVars)
Definition aigOper.c:495
Aig_Obj_t * Aig_IthVar(Aig_Man_t *p, int i)
FUNCTION DEFINITIONS ///.
Definition aigOper.c:63
Aig_Obj_t * Aig_TableLookupInt(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:275
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:259
Aig_Obj_t * Aig_MiterTwo(Aig_Man_t *p, Vec_Ptr_t *vNodes1, Vec_Ptr_t *vNodes2)
Definition aigOper.c:453
void Aig_MuxTest()
Definition aigOper.c:537
Aig_Obj_t * Aig_ObjCreate(Aig_Man_t *p, Aig_Obj_t *pGhost)
Definition aigObj.c:89
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
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
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
int Aig_ManCleanup(Aig_Man_t *p)
Definition aigMan.c:265
Aig_Obj_t * Aig_TableLookup(Aig_Man_t *p, Aig_Obj_t *pGhost)
Definition aigTable.c:116
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigObj.c:45
Aig_Type_t
Definition aig.h:57
@ AIG_OBJ_AND
Definition aig.h:63
@ AIG_OBJ_EXOR
Definition aig.h:64
void Aig_ManDumpBlif(Aig_Man_t *p, char *pFileName, Vec_Ptr_t *vPiNames, Vec_Ptr_t *vPoNames)
Definition aigUtil.c:746
Cube * p
Definition exorList.c:222
#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