abc70930: src/aig/aig/aigOper.c Source File

00001 
00021 #include "aig.h"
00022 
00026 
00027 // procedure to detect an EXOR gate
00028 static inline int Aig_ObjIsExorType( Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 )
00029 {
00030     if ( !Aig_IsComplement(p0) || !Aig_IsComplement(p1) )
00031         return 0;
00032     p0 = Aig_Regular(p0);
00033     p1 = Aig_Regular(p1);
00034     if ( !Aig_ObjIsAnd(p0) || !Aig_ObjIsAnd(p1) )
00035         return 0;
00036     if ( Aig_ObjFanin0(p0) != Aig_ObjFanin0(p1) || Aig_ObjFanin1(p0) != Aig_ObjFanin1(p1) )
00037         return 0;
00038     if ( Aig_ObjFaninC0(p0) == Aig_ObjFaninC0(p1) || Aig_ObjFaninC1(p0) == Aig_ObjFaninC1(p1) )
00039         return 0;
00040     *ppFan0 = Aig_ObjChild0(p0);
00041     *ppFan1 = Aig_ObjChild1(p0);
00042     return 1;
00043 }
00044 
00048 
00060 Aig_Obj_t * Aig_IthVar( Aig_Man_t * p, int i )
00061 {
00062     int v;
00063     for ( v = Aig_ManPiNum(p); v <= i; v++ )
00064         Aig_ObjCreatePi( p );
00065     assert( i < Vec_PtrSize(p->vPis) );
00066     return Aig_ManPi( p, i );
00067 }
00068 
00080 Aig_Obj_t * Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type )
00081 {
00082     if ( Type == AIG_OBJ_AND )
00083         return Aig_And( p, p0, p1 );
00084     if ( Type == AIG_OBJ_EXOR )
00085         return Aig_Exor( p, p0, p1 );
00086     assert( 0 );
00087     return NULL;
00088 }
00089 
00101 Aig_Obj_t * Aig_CanonPair_rec( Aig_Man_t * p, Aig_Obj_t * pGhost )
00102 {
00103     Aig_Obj_t * pResult, * pLat0, * pLat1;
00104     int fCompl0, fCompl1;
00105     Aig_Type_t Type;
00106     assert( Aig_ObjIsNode(pGhost) );
00107     // consider the case when the pair is canonical
00108     if ( !Aig_ObjIsLatch(Aig_ObjFanin0(pGhost)) || !Aig_ObjIsLatch(Aig_ObjFanin1(pGhost)) )
00109     {
00110         if ( (pResult = Aig_TableLookup( p, pGhost )) )
00111             return pResult;
00112         return Aig_ObjCreate( p, pGhost );
00113     }
00115     pLat0 = Aig_ObjFanin0(pGhost);
00116     pLat1 = Aig_ObjFanin1(pGhost);
00117     // remember type and compls
00118     Type = Aig_ObjType(pGhost);
00119     fCompl0 = Aig_ObjFaninC0(pGhost);
00120     fCompl1 = Aig_ObjFaninC1(pGhost);
00121     // call recursively
00122     pResult = Aig_Oper( p, Aig_NotCond(Aig_ObjChild0(pLat0), fCompl0), Aig_NotCond(Aig_ObjChild0(pLat1), fCompl1), Type );
00123     // build latch on top of this
00124     return Aig_Latch( p, pResult, (Type == AIG_OBJ_AND)? fCompl0 & fCompl1 : fCompl0 ^ fCompl1 );
00125 }
00126 
00138 Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
00139 {
00140     Aig_Obj_t * pGhost, * pResult;
00141 //    Aig_Obj_t * pFan0, * pFan1;
00142     // check trivial cases
00143     if ( p0 == p1 )
00144         return p0;
00145     if ( p0 == Aig_Not(p1) )
00146         return Aig_Not(p->pConst1);
00147     if ( Aig_Regular(p0) == p->pConst1 )
00148         return p0 == p->pConst1 ? p1 : Aig_Not(p->pConst1);
00149     if ( Aig_Regular(p1) == p->pConst1 )
00150         return p1 == p->pConst1 ? p0 : Aig_Not(p->pConst1);
00151     // check not so trivial cases
00152     if ( p->fAddStrash && (Aig_ObjIsNode(Aig_Regular(p0)) || Aig_ObjIsNode(Aig_Regular(p1))) )
00153     { // http://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf
00154         Aig_Obj_t * pFanA, * pFanB, * pFanC, * pFanD;
00155         pFanA = Aig_ObjChild0(Aig_Regular(p0));
00156         pFanB = Aig_ObjChild1(Aig_Regular(p0));
00157         pFanC = Aig_ObjChild0(Aig_Regular(p1));
00158         pFanD = Aig_ObjChild1(Aig_Regular(p1));
00159         if ( Aig_IsComplement(p0) )
00160         {
00161             if ( pFanA == Aig_Not(p1) || pFanB == Aig_Not(p1) )
00162                 return p1;
00163             if ( pFanB == p1 )
00164                 return Aig_And( p, Aig_Not(pFanA), pFanB );
00165             if ( pFanA == p1 )
00166                 return Aig_And( p, Aig_Not(pFanB), pFanA );
00167         }
00168         else
00169         {
00170             if ( pFanA == Aig_Not(p1) || pFanB == Aig_Not(p1) )
00171                 return Aig_Not(p->pConst1);
00172             if ( pFanA == p1 || pFanB == p1 )
00173                 return p0;
00174         }
00175         if ( Aig_IsComplement(p1) )
00176         {
00177             if ( pFanC == Aig_Not(p0) || pFanD == Aig_Not(p0) )
00178                 return p0;
00179             if ( pFanD == p0 )
00180                 return Aig_And( p, Aig_Not(pFanC), pFanD );
00181             if ( pFanC == p0 )
00182                 return Aig_And( p, Aig_Not(pFanD), pFanC );
00183         }
00184         else
00185         {
00186             if ( pFanC == Aig_Not(p0) || pFanD == Aig_Not(p0) )
00187                 return Aig_Not(p->pConst1);
00188             if ( pFanC == p0 || pFanD == p0 )
00189                 return p1;
00190         }
00191         if ( !Aig_IsComplement(p0) && !Aig_IsComplement(p1) ) 
00192         {
00193             if ( pFanA == Aig_Not(pFanC) || pFanA == Aig_Not(pFanD) || pFanB == Aig_Not(pFanC) || pFanB == Aig_Not(pFanD) )
00194                 return Aig_Not(p->pConst1);
00195             if ( pFanA == pFanC || pFanB == pFanC )
00196                 return Aig_And( p, p0, pFanD );
00197             if ( pFanB == pFanC || pFanB == pFanD )
00198                 return Aig_And( p, pFanA, p1 );
00199             if ( pFanA == pFanD || pFanB == pFanD )
00200                 return Aig_And( p, p0, pFanC );
00201             if ( pFanA == pFanC || pFanA == pFanD )
00202                 return Aig_And( p, pFanB, p1 );
00203         }
00204         else if ( Aig_IsComplement(p0) && !Aig_IsComplement(p1) )
00205         {
00206             if ( pFanA == Aig_Not(pFanC) || pFanA == Aig_Not(pFanD) || pFanB == Aig_Not(pFanC) || pFanB == Aig_Not(pFanD) )
00207                 return p1;
00208             if ( pFanB == pFanC || pFanB == pFanD )
00209                 return Aig_And( p, Aig_Not(pFanA), p1 );
00210             if ( pFanA == pFanC || pFanA == pFanD )
00211                 return Aig_And( p, Aig_Not(pFanB), p1 );
00212         }
00213         else if ( !Aig_IsComplement(p0) && Aig_IsComplement(p1) )
00214         {
00215             if ( pFanC == Aig_Not(pFanA) || pFanC == Aig_Not(pFanB) || pFanD == Aig_Not(pFanA) || pFanD == Aig_Not(pFanB) )
00216                 return p0;
00217             if ( pFanD == pFanA || pFanD == pFanB )
00218                 return Aig_And( p, Aig_Not(pFanC), p0 );
00219             if ( pFanC == pFanA || pFanC == pFanB )
00220                 return Aig_And( p, Aig_Not(pFanD), p0 );
00221         }
00222         else // if ( Aig_IsComplement(p0) && Aig_IsComplement(p1) )
00223         {
00224             if ( pFanA == pFanD && pFanB == Aig_Not(pFanC) )
00225                 return Aig_Not(pFanA);
00226             if ( pFanB == pFanC && pFanA == Aig_Not(pFanD) )
00227                 return Aig_Not(pFanB);
00228             if ( pFanA == pFanC && pFanB == Aig_Not(pFanD) )
00229                 return Aig_Not(pFanA);
00230             if ( pFanB == pFanD && pFanA == Aig_Not(pFanC) )
00231                 return Aig_Not(pFanB);
00232         }
00233     }
00234     // check if it can be an EXOR gate
00235 //    if ( Aig_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
00236 //        return Aig_Exor( p, pFan0, pFan1 );
00237     pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_AND );
00238     pResult = Aig_CanonPair_rec( p, pGhost );
00239     return pResult;
00240 }
00241 
00253 Aig_Obj_t * Aig_Latch( Aig_Man_t * p, Aig_Obj_t * pObj, int fInitOne )
00254 {
00255     Aig_Obj_t * pGhost, * pResult;
00256     pGhost = Aig_ObjCreateGhost( p, Aig_NotCond(pObj, fInitOne), NULL, AIG_OBJ_LATCH );
00257     pResult = Aig_TableLookup( p, pGhost );
00258     if ( pResult == NULL )
00259         pResult = Aig_ObjCreate( p, pGhost );
00260     return Aig_NotCond( pResult, fInitOne );
00261 }
00262 
00274 Aig_Obj_t * Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
00275 {
00276 /*
00277     Aig_Obj_t * pGhost, * pResult;
00278     // check trivial cases
00279     if ( p0 == p1 )
00280         return Aig_Not(p->pConst1);
00281     if ( p0 == Aig_Not(p1) )
00282         return p->pConst1;
00283     if ( Aig_Regular(p0) == p->pConst1 )
00284         return Aig_NotCond( p1, p0 == p->pConst1 );
00285     if ( Aig_Regular(p1) == p->pConst1 )
00286         return Aig_NotCond( p0, p1 == p->pConst1 );
00287     // check the table
00288     pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_EXOR );
00289     if ( pResult = Aig_TableLookup( p, pGhost ) )
00290         return pResult;
00291     return Aig_ObjCreate( p, pGhost );
00292 */
00293     return Aig_Or( p, Aig_And(p, p0, Aig_Not(p1)), Aig_And(p, Aig_Not(p0), p1) );
00294 }
00295 
00307 Aig_Obj_t * Aig_Or( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
00308 {
00309     return Aig_Not( Aig_And( p, Aig_Not(p0), Aig_Not(p1) ) );
00310 }
00311 
00323 Aig_Obj_t * Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 )
00324 {
00325 /*    
00326     Aig_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp;
00327     int Count0, Count1;
00328     // consider trivial cases
00329     if ( p0 == Aig_Not(p1) )
00330         return Aig_Exor( p, pC, p0 );
00331     // other cases can be added
00332     // implement the first MUX (F = C * x1 + C' * x0)
00333 
00334     // check for constants here!!!
00335 
00336     pTempA1 = Aig_TableLookup( p, Aig_ObjCreateGhost(p, pC,          p1, AIG_OBJ_AND) );
00337     pTempA2 = Aig_TableLookup( p, Aig_ObjCreateGhost(p, Aig_Not(pC), p0, AIG_OBJ_AND) );
00338     if ( pTempA1 && pTempA2 )
00339     {
00340         pTemp = Aig_TableLookup( p, Aig_ObjCreateGhost(p, Aig_Not(pTempA1), Aig_Not(pTempA2), AIG_OBJ_AND) );
00341         if ( pTemp ) return Aig_Not(pTemp);
00342     }
00343     Count0 = (pTempA1 != NULL) + (pTempA2 != NULL);
00344     // implement the second MUX (F' = C * x1' + C' * x0')
00345     pTempB1 = Aig_TableLookup( p, Aig_ObjCreateGhost(p, pC,          Aig_Not(p1), AIG_OBJ_AND) );
00346     pTempB2 = Aig_TableLookup( p, Aig_ObjCreateGhost(p, Aig_Not(pC), Aig_Not(p0), AIG_OBJ_AND) );
00347     if ( pTempB1 && pTempB2 )
00348     {
00349         pTemp = Aig_TableLookup( p, Aig_ObjCreateGhost(p, Aig_Not(pTempB1), Aig_Not(pTempB2), AIG_OBJ_AND) );
00350         if ( pTemp ) return pTemp;
00351     }
00352     Count1 = (pTempB1 != NULL) + (pTempB2 != NULL);
00353     // compare and decide which one to implement
00354     if ( Count0 >= Count1 )
00355     {
00356         pTempA1 = pTempA1? pTempA1 : Aig_And(p, pC,          p1);
00357         pTempA2 = pTempA2? pTempA2 : Aig_And(p, Aig_Not(pC), p0);
00358         return Aig_Or( p, pTempA1, pTempA2 );
00359     }
00360     pTempB1 = pTempB1? pTempB1 : Aig_And(p, pC,          Aig_Not(p1));
00361     pTempB2 = pTempB2? pTempB2 : Aig_And(p, Aig_Not(pC), Aig_Not(p0));
00362     return Aig_Not( Aig_Or( p, pTempB1, pTempB2 ) );
00363 */
00364     return Aig_Or( p, Aig_And(p, pC, p1), Aig_And(p, Aig_Not(pC), p0) );
00365 }
00366 
00378 Aig_Obj_t * Aig_Maj( Aig_Man_t * p, Aig_Obj_t * pA, Aig_Obj_t * pB, Aig_Obj_t * pC )
00379 {
00380     return Aig_Or( p, Aig_Or(p, Aig_And(p, pA, pB), Aig_And(p, pA, pC)), Aig_And(p, pB, pC) );
00381 }
00382 
00394 Aig_Obj_t * Aig_Multi_rec( Aig_Man_t * p, Aig_Obj_t ** ppObjs, int nObjs, Aig_Type_t Type )
00395 {
00396     Aig_Obj_t * pObj1, * pObj2;
00397     if ( nObjs == 1 )
00398         return ppObjs[0];
00399     pObj1 = Aig_Multi_rec( p, ppObjs,           nObjs/2,         Type );
00400     pObj2 = Aig_Multi_rec( p, ppObjs + nObjs/2, nObjs - nObjs/2, Type );
00401     return Aig_Oper( p, pObj1, pObj2, Type );
00402 }
00403 
00415 Aig_Obj_t * Aig_Multi( Aig_Man_t * p, Aig_Obj_t ** pArgs, int nArgs, Aig_Type_t Type )
00416 {
00417     assert( Type == AIG_OBJ_AND || Type == AIG_OBJ_EXOR );
00418     assert( nArgs > 0 );
00419     return Aig_Multi_rec( p, pArgs, nArgs, Type );
00420 }
00421 
00433 Aig_Obj_t * Aig_Miter( Aig_Man_t * p, Vec_Ptr_t * vPairs )
00434 {
00435     int i;
00436     assert( vPairs->nSize > 0 );
00437     assert( vPairs->nSize % 2 == 0 );
00438     for ( i = 0; i < vPairs->nSize; i += 2 )
00439         vPairs->pArray[i/2] = Aig_Not( Aig_Exor( p, vPairs->pArray[i], vPairs->pArray[i+1] ) );
00440     vPairs->nSize = vPairs->nSize/2;
00441     return Aig_Not( Aig_Multi_rec( p, (Aig_Obj_t **)vPairs->pArray, vPairs->nSize, AIG_OBJ_AND ) );
00442 }
00443 
00455 Aig_Obj_t * Aig_MiterTwo( Aig_Man_t * p, Vec_Ptr_t * vNodes1, Vec_Ptr_t * vNodes2 )
00456 {
00457     int i;
00458     assert( vNodes1->nSize > 0 && vNodes1->nSize > 0 );
00459     assert( vNodes1->nSize == vNodes2->nSize );
00460     for ( i = 0; i < vNodes1->nSize; i++ )
00461         vNodes1->pArray[i] = Aig_Not( Aig_Exor( p, vNodes1->pArray[i], vNodes2->pArray[i] ) );
00462     return Aig_Not( Aig_Multi_rec( p, (Aig_Obj_t **)vNodes1->pArray, vNodes1->nSize, AIG_OBJ_AND ) );
00463 }
00464 
00476 Aig_Obj_t * Aig_CreateAnd( Aig_Man_t * p, int nVars )
00477 {
00478     Aig_Obj_t * pFunc;
00479     int i;
00480     pFunc = Aig_ManConst1( p );
00481     for ( i = 0; i < nVars; i++ )
00482         pFunc = Aig_And( p, pFunc, Aig_IthVar(p, i) );
00483     return pFunc;
00484 }
00485 
00497 Aig_Obj_t * Aig_CreateOr( Aig_Man_t * p, int nVars )
00498 {
00499     Aig_Obj_t * pFunc;
00500     int i;
00501     pFunc = Aig_ManConst0( p );
00502     for ( i = 0; i < nVars; i++ )
00503         pFunc = Aig_Or( p, pFunc, Aig_IthVar(p, i) );
00504     return pFunc;
00505 }
00506 
00518 Aig_Obj_t * Aig_CreateExor( Aig_Man_t * p, int nVars )
00519 {
00520     Aig_Obj_t * pFunc;
00521     int i;
00522     pFunc = Aig_ManConst0( p );
00523     for ( i = 0; i < nVars; i++ )
00524         pFunc = Aig_Exor( p, pFunc, Aig_IthVar(p, i) );
00525     return pFunc;
00526 }
00527 
00531 
00532