src/aig/dar/darBalance.c File Reference

#include "darInt.h"
Include dependency graph for darBalance.c:

Go to the source code of this file.

Functions

static Aig_Obj_t * Dar_Balance_rec (Aig_Man_t *pNew, Aig_Obj_t *pObj, Vec_Vec_t *vStore, int Level, int fUpdateLevel)
static Vec_Ptr_t * Dar_BalanceCone (Aig_Obj_t *pObj, Vec_Vec_t *vStore, int Level)
static int Dar_BalanceFindLeft (Vec_Ptr_t *vSuper)
static void Dar_BalancePermute (Aig_Man_t *p, Vec_Ptr_t *vSuper, int LeftBound, int fExor)
static void Dar_BalancePushUniqueOrderByLevel (Vec_Ptr_t *vStore, Aig_Obj_t *pObj)
static Aig_Obj_t * Dar_BalanceBuildSuper (Aig_Man_t *p, Vec_Ptr_t *vSuper, Aig_Type_t Type, int fUpdateLevel)
Aig_Man_t * Dar_ManBalance (Aig_Man_t *p, int fUpdateLevel)
int Dar_BalanceCone_rec (Aig_Obj_t *pRoot, Aig_Obj_t *pObj, Vec_Ptr_t *vSuper)
int Aig_NodeCompareLevelsDecrease (Aig_Obj_t **pp1, Aig_Obj_t **pp2)

Function Documentation

int Aig_NodeCompareLevelsDecrease ( Aig_Obj_t **  pp1,
Aig_Obj_t **  pp2 
)

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

Synopsis [Procedure used for sorting the nodes in decreasing order of levels.]

Description []

SideEffects []

SeeAlso []

Definition at line 221 of file darBalance.c.

00222 {
00223     int Diff = Aig_ObjLevel(Aig_Regular(*pp1)) - Aig_ObjLevel(Aig_Regular(*pp2));
00224     if ( Diff > 0 )
00225         return -1;
00226     if ( Diff < 0 ) 
00227         return 1;
00228     return 0; 
00229 }

Aig_Obj_t * Dar_Balance_rec ( Aig_Man_t *  pNew,
Aig_Obj_t *  pObjOld,
Vec_Vec_t *  vStore,
int  Level,
int  fUpdateLevel 
) [static]

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

FileName [darBalance.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting.]

Synopsis [Algebraic AIG balancing.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

] DECLARATIONS ///

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

Synopsis [Returns the new node constructed.]

Description []

SideEffects []

SeeAlso []

Definition at line 97 of file darBalance.c.

00098 {
00099     Aig_Obj_t * pObjNew;
00100     Vec_Ptr_t * vSuper;
00101     int i;
00102     assert( !Aig_IsComplement(pObjOld) );
00103     assert( !Aig_ObjIsBuf(pObjOld) );
00104     // return if the result is known
00105     if ( pObjOld->pData )
00106         return pObjOld->pData;
00107     assert( Aig_ObjIsNode(pObjOld) );
00108     // get the implication supergate
00109     vSuper = Dar_BalanceCone( pObjOld, vStore, Level );
00110     // check if supergate contains two nodes in the opposite polarity
00111     if ( vSuper->nSize == 0 )
00112         return pObjOld->pData = Aig_ManConst0(pNew);
00113     if ( Vec_PtrSize(vSuper) < 2 )
00114         printf( "BUG!\n" );
00115     // for each old node, derive the new well-balanced node
00116     for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
00117     {
00118         pObjNew = Dar_Balance_rec( pNew, Aig_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
00119         vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement(vSuper->pArray[i]) );
00120     }
00121     // build the supergate
00122     pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel );
00123     // make sure the balanced node is not assigned
00124 //    assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
00125     assert( pObjOld->pData == NULL );
00126     return pObjOld->pData = pObjNew;
00127 }

Aig_Obj_t * Dar_BalanceBuildSuper ( Aig_Man_t *  p,
Vec_Ptr_t *  vSuper,
Aig_Type_t  Type,
int  fUpdateLevel 
) [static]

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

Synopsis [Builds implication supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 242 of file darBalance.c.

00243 {
00244     Aig_Obj_t * pObj1, * pObj2;
00245     int LeftBound;
00246     assert( vSuper->nSize > 1 );
00247     // sort the new nodes by level in the decreasing order
00248     Vec_PtrSort( vSuper, Aig_NodeCompareLevelsDecrease );
00249     // balance the nodes
00250     while ( vSuper->nSize > 1 )
00251     {
00252         // find the left bound on the node to be paired
00253         LeftBound = (!fUpdateLevel)? 0 : Dar_BalanceFindLeft( vSuper );
00254         // find the node that can be shared (if no such node, randomize choice)
00255         Dar_BalancePermute( p, vSuper, LeftBound, Type == AIG_OBJ_EXOR );
00256         // pull out the last two nodes
00257         pObj1 = Vec_PtrPop(vSuper);
00258         pObj2 = Vec_PtrPop(vSuper);
00259         Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type) );
00260     }
00261     return Vec_PtrEntry(vSuper, 0);
00262 }

Vec_Ptr_t * Dar_BalanceCone ( Aig_Obj_t *  pObj,
Vec_Vec_t *  vStore,
int  Level 
) [static]

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

Synopsis [Collects the nodes of the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 186 of file darBalance.c.

00187 {
00188     Vec_Ptr_t * vNodes;
00189     int RetValue, i;
00190     assert( !Aig_IsComplement(pObj) );
00191     // extend the storage
00192     if ( Vec_VecSize( vStore ) <= Level )
00193         Vec_VecPush( vStore, Level, 0 );
00194     // get the temporary array of nodes
00195     vNodes = Vec_VecEntry( vStore, Level );
00196     Vec_PtrClear( vNodes );
00197     // collect the nodes in the implication supergate
00198     RetValue = Dar_BalanceCone_rec( pObj, pObj, vNodes );
00199     assert( vNodes->nSize > 1 );
00200     // unmark the visited nodes
00201     Vec_PtrForEachEntry( vNodes, pObj, i )
00202         Aig_Regular(pObj)->fMarkB = 0;
00203     // if we found the node and its complement in the same implication supergate, 
00204     // return empty set of nodes (meaning that we should use constant-0 node)
00205     if ( RetValue == -1 )
00206         vNodes->nSize = 0;
00207     return vNodes;
00208 }

int Dar_BalanceCone_rec ( Aig_Obj_t *  pRoot,
Aig_Obj_t *  pObj,
Vec_Ptr_t *  vSuper 
)

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

Synopsis [Collects the nodes of the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file darBalance.c.

00141 {
00142     int RetValue1, RetValue2, i;
00143     // check if the node is visited
00144     if ( Aig_Regular(pObj)->fMarkB )
00145     {
00146         // check if the node occurs in the same polarity
00147         for ( i = 0; i < vSuper->nSize; i++ )
00148             if ( vSuper->pArray[i] == pObj )
00149                 return 1;
00150         // check if the node is present in the opposite polarity
00151         for ( i = 0; i < vSuper->nSize; i++ )
00152             if ( vSuper->pArray[i] == Aig_Not(pObj) )
00153                 return -1;
00154         assert( 0 );
00155         return 0;
00156     }
00157     // if the new node is complemented or a PI, another gate begins
00158     if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1) )
00159     {
00160         Vec_PtrPush( vSuper, pObj );
00161         Aig_Regular(pObj)->fMarkB = 1;
00162         return 0;
00163     }
00164     assert( !Aig_IsComplement(pObj) );
00165     assert( Aig_ObjIsNode(pObj) );
00166     // go through the branches
00167     RetValue1 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
00168     RetValue2 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
00169     if ( RetValue1 == -1 || RetValue2 == -1 )
00170         return -1;
00171     // return 1 if at least one branch has a duplicate
00172     return RetValue1 || RetValue2;
00173 }

int Dar_BalanceFindLeft ( Vec_Ptr_t *  vSuper  )  [static]

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

Synopsis [Finds the left bound on the next candidate to be paired.]

Description [The nodes in the array are in the decreasing order of levels. The last node in the array has the smallest level. By default it would be paired with the next node on the left. However, it may be possible to pair it with some other node on the left, in such a way that the new node is shared. This procedure finds the index of the left-most node, which can be paired with the last node.]

SideEffects []

SeeAlso []

Definition at line 279 of file darBalance.c.

00280 {
00281     Aig_Obj_t * pObjRight, * pObjLeft;
00282     int Current;
00283     // if two or less nodes, pair with the first
00284     if ( Vec_PtrSize(vSuper) < 3 )
00285         return 0;
00286     // set the pointer to the one before the last
00287     Current = Vec_PtrSize(vSuper) - 2;
00288     pObjRight = Vec_PtrEntry( vSuper, Current );
00289     // go through the nodes to the left of this one
00290     for ( Current--; Current >= 0; Current-- )
00291     {
00292         // get the next node on the left
00293         pObjLeft = Vec_PtrEntry( vSuper, Current );
00294         // if the level of this node is different, quit the loop
00295         if ( Aig_ObjLevel(Aig_Regular(pObjLeft)) != Aig_ObjLevel(Aig_Regular(pObjRight)) )
00296             break;
00297     }
00298     Current++;    
00299     // get the node, for which the equality holds
00300     pObjLeft = Vec_PtrEntry( vSuper, Current );
00301     assert( Aig_ObjLevel(Aig_Regular(pObjLeft)) == Aig_ObjLevel(Aig_Regular(pObjRight)) );
00302     return Current;
00303 }

void Dar_BalancePermute ( Aig_Man_t *  p,
Vec_Ptr_t *  vSuper,
int  LeftBound,
int  fExor 
) [static]

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

Synopsis [Moves closer to the end the node that is best for sharing.]

Description [If there is no node with sharing, randomly chooses one of the legal nodes.]

SideEffects []

SeeAlso []

Definition at line 317 of file darBalance.c.

00318 {
00319     Aig_Obj_t * pObj1, * pObj2, * pObj3, * pGhost;
00320     int RightBound, i;
00321     // get the right bound
00322     RightBound = Vec_PtrSize(vSuper) - 2;
00323     assert( LeftBound <= RightBound );
00324     if ( LeftBound == RightBound )
00325         return;
00326     // get the two last nodes
00327     pObj1 = Vec_PtrEntry( vSuper, RightBound + 1 );
00328     pObj2 = Vec_PtrEntry( vSuper, RightBound     );
00329     if ( Aig_Regular(pObj1) == p->pConst1 || Aig_Regular(pObj2) == p->pConst1 )
00330         return;
00331     // find the first node that can be shared
00332     for ( i = RightBound; i >= LeftBound; i-- )
00333     {
00334         pObj3 = Vec_PtrEntry( vSuper, i );
00335         if ( Aig_Regular(pObj3) == p->pConst1 )
00336         {
00337             Vec_PtrWriteEntry( vSuper, i,          pObj2 );
00338             Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
00339             return;
00340         }
00341         pGhost = Aig_ObjCreateGhost( p, pObj1, pObj3, fExor? AIG_OBJ_EXOR : AIG_OBJ_AND );
00342         if ( Aig_TableLookup( p, pGhost ) )
00343         {
00344             if ( pObj3 == pObj2 )
00345                 return;
00346             Vec_PtrWriteEntry( vSuper, i,          pObj2 );
00347             Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
00348             return;
00349         }
00350     }
00351 /*
00352     // we did not find the node to share, randomize choice
00353     {
00354         int Choice = rand() % (RightBound - LeftBound + 1);
00355         pObj3 = Vec_PtrEntry( vSuper, LeftBound + Choice );
00356         if ( pObj3 == pObj2 )
00357             return;
00358         Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pObj2 );
00359         Vec_PtrWriteEntry( vSuper, RightBound,         pObj3 );
00360     }
00361 */
00362 }

void Dar_BalancePushUniqueOrderByLevel ( Vec_Ptr_t *  vStore,
Aig_Obj_t *  pObj 
) [static]

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

Synopsis [Inserts a new node in the order by levels.]

Description []

SideEffects []

SeeAlso []

Definition at line 375 of file darBalance.c.

00376 {
00377     Aig_Obj_t * pObj1, * pObj2;
00378     int i;
00379     if ( Vec_PtrPushUnique(vStore, pObj) )
00380         return;
00381     // find the p of the node
00382     for ( i = vStore->nSize-1; i > 0; i-- )
00383     {
00384         pObj1 = vStore->pArray[i  ];
00385         pObj2 = vStore->pArray[i-1];
00386         if ( Aig_ObjLevel(Aig_Regular(pObj1)) <= Aig_ObjLevel(Aig_Regular(pObj2)) )
00387             break;
00388         vStore->pArray[i  ] = pObj2;
00389         vStore->pArray[i-1] = pObj1;
00390     }
00391 }

Aig_Man_t* Dar_ManBalance ( Aig_Man_t *  p,
int  fUpdateLevel 
)

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

Synopsis [Performs algebraic balancing of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 49 of file darBalance.c.

00050 {
00051     Aig_Man_t * pNew;
00052     Aig_Obj_t * pObj, * pDriver, * pObjNew;
00053     Vec_Vec_t * vStore;
00054     int i;
00055     // create the new manager 
00056     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
00057     pNew->pName = Aig_UtilStrsav( p->pName );
00058     pNew->nRegs = p->nRegs;
00059     pNew->nAsserts = p->nAsserts;
00060     if ( p->vFlopNums )
00061         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
00062     // map the PI nodes
00063     Aig_ManCleanData( p );
00064     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
00065     Aig_ManForEachPi( p, pObj, i )
00066         pObj->pData = Aig_ObjCreatePi(pNew);
00067     // balance the AIG
00068     vStore = Vec_VecAlloc( 50 );
00069     Aig_ManForEachPo( p, pObj, i )
00070     {
00071         pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
00072         pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
00073         pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
00074         Aig_ObjCreatePo( pNew, pObjNew );
00075     }
00076     Vec_VecFree( vStore );
00077     // remove dangling nodes
00078     if ( (i = Aig_ManCleanup( pNew )) )
00079         printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
00080     // check the resulting AIG
00081     if ( !Aig_ManCheck(pNew) )
00082         printf( "Dar_ManBalance(): The check has failed.\n" );
00083     return pNew;
00084 }

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