src/aig/aig/aigOper.c File Reference

#include "aig.h"
Include dependency graph for aigOper.c:

Go to the source code of this file.

Functions

static int Aig_ObjIsExorType (Aig_Obj_t *p0, Aig_Obj_t *p1, Aig_Obj_t **ppFan0, Aig_Obj_t **ppFan1)
Aig_Obj_t * Aig_IthVar (Aig_Man_t *p, int i)
Aig_Obj_t * Aig_Oper (Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1, Aig_Type_t Type)
Aig_Obj_t * Aig_CanonPair_rec (Aig_Man_t *p, Aig_Obj_t *pGhost)
Aig_Obj_t * Aig_And (Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Aig_Obj_t * Aig_Latch (Aig_Man_t *p, Aig_Obj_t *pObj, int fInitOne)
Aig_Obj_t * Aig_Exor (Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Aig_Obj_t * Aig_Or (Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Aig_Obj_t * Aig_Mux (Aig_Man_t *p, Aig_Obj_t *pC, Aig_Obj_t *p1, Aig_Obj_t *p0)
Aig_Obj_t * Aig_Maj (Aig_Man_t *p, Aig_Obj_t *pA, Aig_Obj_t *pB, Aig_Obj_t *pC)
Aig_Obj_t * Aig_Multi_rec (Aig_Man_t *p, Aig_Obj_t **ppObjs, int nObjs, Aig_Type_t Type)
Aig_Obj_t * Aig_Multi (Aig_Man_t *p, Aig_Obj_t **pArgs, int nArgs, Aig_Type_t Type)
Aig_Obj_t * Aig_Miter (Aig_Man_t *p, Vec_Ptr_t *vPairs)
Aig_Obj_t * Aig_MiterTwo (Aig_Man_t *p, Vec_Ptr_t *vNodes1, Vec_Ptr_t *vNodes2)
Aig_Obj_t * Aig_CreateAnd (Aig_Man_t *p, int nVars)
Aig_Obj_t * Aig_CreateOr (Aig_Man_t *p, int nVars)
Aig_Obj_t * Aig_CreateExor (Aig_Man_t *p, int nVars)

Function Documentation

Aig_Obj_t* Aig_And ( Aig_Man_t *  p,
Aig_Obj_t *  p0,
Aig_Obj_t *  p1 
)

Function*************************************************************

Synopsis [Performs canonicization step.]

Description [The argument nodes can be complemented.]

SideEffects []

SeeAlso []

Definition at line 138 of file aigOper.c.

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 }

Aig_Obj_t* Aig_CanonPair_rec ( Aig_Man_t *  p,
Aig_Obj_t *  pGhost 
)

Function*************************************************************

Synopsis [Creates the canonical form of the node.]

Description []

SideEffects []

SeeAlso []

remember the latches

Definition at line 101 of file aigOper.c.

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 }

Aig_Obj_t* Aig_CreateAnd ( Aig_Man_t *  p,
int  nVars 
)

Function*************************************************************

Synopsis [Creates AND function with nVars inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 476 of file aigOper.c.

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 }

Aig_Obj_t* Aig_CreateExor ( Aig_Man_t *  p,
int  nVars 
)

Function*************************************************************

Synopsis [Creates AND function with nVars inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 518 of file aigOper.c.

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 }

Aig_Obj_t* Aig_CreateOr ( Aig_Man_t *  p,
int  nVars 
)

Function*************************************************************

Synopsis [Creates AND function with nVars inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 497 of file aigOper.c.

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 }

Aig_Obj_t* Aig_Exor ( Aig_Man_t *  p,
Aig_Obj_t *  p0,
Aig_Obj_t *  p1 
)

Function*************************************************************

Synopsis [Performs canonicization step.]

Description [The argument nodes can be complemented.]

SideEffects []

SeeAlso []

Definition at line 274 of file aigOper.c.

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 }

Aig_Obj_t* Aig_IthVar ( Aig_Man_t *  p,
int  i 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Returns i-th elementary variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 60 of file aigOper.c.

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 }

Aig_Obj_t* Aig_Latch ( Aig_Man_t *  p,
Aig_Obj_t *  pObj,
int  fInitOne 
)

Function*************************************************************

Synopsis [Creates the canonical form of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 253 of file aigOper.c.

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 }

Aig_Obj_t* Aig_Maj ( Aig_Man_t *  p,
Aig_Obj_t *  pA,
Aig_Obj_t *  pB,
Aig_Obj_t *  pC 
)

Function*************************************************************

Synopsis [Implements ITE operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 378 of file aigOper.c.

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 }

Aig_Obj_t* Aig_Miter ( Aig_Man_t *  p,
Vec_Ptr_t *  vPairs 
)

Function*************************************************************

Synopsis [Implements the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 433 of file aigOper.c.

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 }

Aig_Obj_t* Aig_MiterTwo ( Aig_Man_t *  p,
Vec_Ptr_t *  vNodes1,
Vec_Ptr_t *  vNodes2 
)

Function*************************************************************

Synopsis [Implements the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 455 of file aigOper.c.

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 }

Aig_Obj_t* Aig_Multi ( Aig_Man_t *  p,
Aig_Obj_t **  pArgs,
int  nArgs,
Aig_Type_t  Type 
)

Function*************************************************************

Synopsis [Old code.]

Description []

SideEffects []

SeeAlso []

Definition at line 415 of file aigOper.c.

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 }

Aig_Obj_t* Aig_Multi_rec ( Aig_Man_t *  p,
Aig_Obj_t **  ppObjs,
int  nObjs,
Aig_Type_t  Type 
)

Function*************************************************************

Synopsis [Constructs the well-balanced tree of gates.]

Description [Disregards levels and possible logic sharing.]

SideEffects []

SeeAlso []

Definition at line 394 of file aigOper.c.

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 }

Aig_Obj_t* Aig_Mux ( Aig_Man_t *  p,
Aig_Obj_t *  pC,
Aig_Obj_t *  p1,
Aig_Obj_t *  p0 
)

Function*************************************************************

Synopsis [Implements ITE operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 323 of file aigOper.c.

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 }

static int Aig_ObjIsExorType ( Aig_Obj_t *  p0,
Aig_Obj_t *  p1,
Aig_Obj_t **  ppFan0,
Aig_Obj_t **  ppFan1 
) [inline, static]

CFile****************************************************************

FileName [aigOper.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG package.]

Synopsis [AIG operations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
aigOper.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

] DECLARATIONS ///

Definition at line 28 of file aigOper.c.

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 }

Aig_Obj_t* Aig_Oper ( Aig_Man_t *  p,
Aig_Obj_t *  p0,
Aig_Obj_t *  p1,
Aig_Type_t  Type 
)

Function*************************************************************

Synopsis [Perform one operation.]

Description [The argument nodes can be complemented.]

SideEffects []

SeeAlso []

Definition at line 80 of file aigOper.c.

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 }

Aig_Obj_t* Aig_Or ( Aig_Man_t *  p,
Aig_Obj_t *  p0,
Aig_Obj_t *  p1 
)

Function*************************************************************

Synopsis [Implements Boolean OR.]

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file aigOper.c.

00308 {
00309     return Aig_Not( Aig_And( p, Aig_Not(p0), Aig_Not(p1) ) );
00310 }

Generated on Tue Jan 5 12:18:11 2010 for abc70930 by  doxygen 1.6.1