src/aig/hop/hopBalance.c File Reference

#include "hop.h"
Include dependency graph for hopBalance.c:

Go to the source code of this file.

Functions

static Hop_Obj_t * Hop_NodeBalance_rec (Hop_Man_t *pNew, Hop_Obj_t *pObj, Vec_Vec_t *vStore, int Level, int fUpdateLevel)
static Vec_Ptr_t * Hop_NodeBalanceCone (Hop_Obj_t *pObj, Vec_Vec_t *vStore, int Level)
static int Hop_NodeBalanceFindLeft (Vec_Ptr_t *vSuper)
static void Hop_NodeBalancePermute (Hop_Man_t *p, Vec_Ptr_t *vSuper, int LeftBound, int fExor)
static void Hop_NodeBalancePushUniqueOrderByLevel (Vec_Ptr_t *vStore, Hop_Obj_t *pObj)
Hop_Man_t * Hop_ManBalance (Hop_Man_t *p, int fUpdateLevel)
int Hop_NodeBalanceCone_rec (Hop_Obj_t *pRoot, Hop_Obj_t *pObj, Vec_Ptr_t *vSuper)
int Hop_NodeCompareLevelsDecrease (Hop_Obj_t **pp1, Hop_Obj_t **pp2)
Hop_Obj_t * Hop_NodeBalanceBuildSuper (Hop_Man_t *p, Vec_Ptr_t *vSuper, Hop_Type_t Type, int fUpdateLevel)

Function Documentation

Hop_Man_t* Hop_ManBalance ( Hop_Man_t *  p,
int  fUpdateLevel 
)

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

Synopsis [Performs algebraic balancing of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file hopBalance.c.

00049 {
00050     Hop_Man_t * pNew;
00051     Hop_Obj_t * pObj, * pObjNew;
00052     Vec_Vec_t * vStore;
00053     int i;
00054     // create the new manager 
00055     pNew = Hop_ManStart();
00056     pNew->fRefCount = 0;
00057     // map the PI nodes
00058     Hop_ManCleanData( p );
00059     Hop_ManConst1(p)->pData = Hop_ManConst1(pNew);
00060     Hop_ManForEachPi( p, pObj, i )
00061         pObj->pData = Hop_ObjCreatePi(pNew);
00062     // balance the AIG
00063     vStore = Vec_VecAlloc( 50 );
00064     Hop_ManForEachPo( p, pObj, i )
00065     {
00066         pObjNew = Hop_NodeBalance_rec( pNew, Hop_ObjFanin0(pObj), vStore, 0, fUpdateLevel );
00067         Hop_ObjCreatePo( pNew, Hop_NotCond( pObjNew, Hop_ObjFaninC0(pObj) ) );
00068     }
00069     Vec_VecFree( vStore );
00070     // remove dangling nodes
00071 //    Hop_ManCreateRefs( pNew );
00072 //    if ( i = Hop_ManCleanup( pNew ) )
00073 //        printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
00074     // check the resulting AIG
00075     if ( !Hop_ManCheck(pNew) )
00076         printf( "Hop_ManBalance(): The check has failed.\n" );
00077     return pNew;
00078 }

Hop_Obj_t * Hop_NodeBalance_rec ( Hop_Man_t *  pNew,
Hop_Obj_t *  pObjOld,
Vec_Vec_t *  vStore,
int  Level,
int  fUpdateLevel 
) [static]

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

FileName [hopBalance.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Minimalistic And-Inverter Graph package.]

Synopsis [Algebraic AIG balancing.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id
hopBalance.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

] DECLARATIONS ///

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

Synopsis [Returns the new node constructed.]

Description []

SideEffects []

SeeAlso []

Definition at line 91 of file hopBalance.c.

00092 {
00093     Hop_Obj_t * pObjNew;
00094     Vec_Ptr_t * vSuper;
00095     int i;
00096     assert( !Hop_IsComplement(pObjOld) );
00097     // return if the result is known
00098     if ( pObjOld->pData )
00099         return pObjOld->pData;
00100     assert( Hop_ObjIsNode(pObjOld) );
00101     // get the implication supergate
00102     vSuper = Hop_NodeBalanceCone( pObjOld, vStore, Level );
00103     // check if supergate contains two nodes in the opposite polarity
00104     if ( vSuper->nSize == 0 )
00105         return pObjOld->pData = Hop_ManConst0(pNew);
00106     if ( Vec_PtrSize(vSuper) < 2 )
00107         printf( "BUG!\n" );
00108     // for each old node, derive the new well-balanced node
00109     for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
00110     {
00111         pObjNew = Hop_NodeBalance_rec( pNew, Hop_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
00112         vSuper->pArray[i] = Hop_NotCond( pObjNew, Hop_IsComplement(vSuper->pArray[i]) );
00113     }
00114     // build the supergate
00115     pObjNew = Hop_NodeBalanceBuildSuper( pNew, vSuper, Hop_ObjType(pObjOld), fUpdateLevel );
00116     // make sure the balanced node is not assigned
00117 //    assert( pObjOld->Level >= Hop_Regular(pObjNew)->Level );
00118     assert( pObjOld->pData == NULL );
00119     return pObjOld->pData = pObjNew;
00120 }

Hop_Obj_t* Hop_NodeBalanceBuildSuper ( Hop_Man_t *  p,
Vec_Ptr_t *  vSuper,
Hop_Type_t  Type,
int  fUpdateLevel 
)

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

Synopsis [Builds implication supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 235 of file hopBalance.c.

00236 {
00237     Hop_Obj_t * pObj1, * pObj2;
00238     int LeftBound;
00239     assert( vSuper->nSize > 1 );
00240     // sort the new nodes by level in the decreasing order
00241     Vec_PtrSort( vSuper, Hop_NodeCompareLevelsDecrease );
00242     // balance the nodes
00243     while ( vSuper->nSize > 1 )
00244     {
00245         // find the left bound on the node to be paired
00246         LeftBound = (!fUpdateLevel)? 0 : Hop_NodeBalanceFindLeft( vSuper );
00247         // find the node that can be shared (if no such node, randomize choice)
00248         Hop_NodeBalancePermute( p, vSuper, LeftBound, Type == AIG_EXOR );
00249         // pull out the last two nodes
00250         pObj1 = Vec_PtrPop(vSuper);
00251         pObj2 = Vec_PtrPop(vSuper);
00252         Hop_NodeBalancePushUniqueOrderByLevel( vSuper, Hop_Oper(p, pObj1, pObj2, Type) );
00253     }
00254     return Vec_PtrEntry(vSuper, 0);
00255 }

Vec_Ptr_t * Hop_NodeBalanceCone ( Hop_Obj_t *  pObj,
Vec_Vec_t *  vStore,
int  Level 
) [static]

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

Synopsis [Collects the nodes of the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 179 of file hopBalance.c.

00180 {
00181     Vec_Ptr_t * vNodes;
00182     int RetValue, i;
00183     assert( !Hop_IsComplement(pObj) );
00184     // extend the storage
00185     if ( Vec_VecSize( vStore ) <= Level )
00186         Vec_VecPush( vStore, Level, 0 );
00187     // get the temporary array of nodes
00188     vNodes = Vec_VecEntry( vStore, Level );
00189     Vec_PtrClear( vNodes );
00190     // collect the nodes in the implication supergate
00191     RetValue = Hop_NodeBalanceCone_rec( pObj, pObj, vNodes );
00192     assert( vNodes->nSize > 1 );
00193     // unmark the visited nodes
00194     Vec_PtrForEachEntry( vNodes, pObj, i )
00195         Hop_Regular(pObj)->fMarkB = 0;
00196     // if we found the node and its complement in the same implication supergate, 
00197     // return empty set of nodes (meaning that we should use constant-0 node)
00198     if ( RetValue == -1 )
00199         vNodes->nSize = 0;
00200     return vNodes;
00201 }

int Hop_NodeBalanceCone_rec ( Hop_Obj_t *  pRoot,
Hop_Obj_t *  pObj,
Vec_Ptr_t *  vSuper 
)

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

Synopsis [Collects the nodes of the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file hopBalance.c.

00134 {
00135     int RetValue1, RetValue2, i;
00136     // check if the node is visited
00137     if ( Hop_Regular(pObj)->fMarkB )
00138     {
00139         // check if the node occurs in the same polarity
00140         for ( i = 0; i < vSuper->nSize; i++ )
00141             if ( vSuper->pArray[i] == pObj )
00142                 return 1;
00143         // check if the node is present in the opposite polarity
00144         for ( i = 0; i < vSuper->nSize; i++ )
00145             if ( vSuper->pArray[i] == Hop_Not(pObj) )
00146                 return -1;
00147         assert( 0 );
00148         return 0;
00149     }
00150     // if the new node is complemented or a PI, another gate begins
00151     if ( pObj != pRoot && (Hop_IsComplement(pObj) || Hop_ObjType(pObj) != Hop_ObjType(pRoot) || Hop_ObjRefs(pObj) > 1) )
00152     {
00153         Vec_PtrPush( vSuper, pObj );
00154         Hop_Regular(pObj)->fMarkB = 1;
00155         return 0;
00156     }
00157     assert( !Hop_IsComplement(pObj) );
00158     assert( Hop_ObjIsNode(pObj) );
00159     // go through the branches
00160     RetValue1 = Hop_NodeBalanceCone_rec( pRoot, Hop_ObjChild0(pObj), vSuper );
00161     RetValue2 = Hop_NodeBalanceCone_rec( pRoot, Hop_ObjChild1(pObj), vSuper );
00162     if ( RetValue1 == -1 || RetValue2 == -1 )
00163         return -1;
00164     // return 1 if at least one branch has a duplicate
00165     return RetValue1 || RetValue2;
00166 }

int Hop_NodeBalanceFindLeft ( 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 272 of file hopBalance.c.

00273 {
00274     Hop_Obj_t * pObjRight, * pObjLeft;
00275     int Current;
00276     // if two or less nodes, pair with the first
00277     if ( Vec_PtrSize(vSuper) < 3 )
00278         return 0;
00279     // set the pointer to the one before the last
00280     Current = Vec_PtrSize(vSuper) - 2;
00281     pObjRight = Vec_PtrEntry( vSuper, Current );
00282     // go through the nodes to the left of this one
00283     for ( Current--; Current >= 0; Current-- )
00284     {
00285         // get the next node on the left
00286         pObjLeft = Vec_PtrEntry( vSuper, Current );
00287         // if the level of this node is different, quit the loop
00288         if ( Hop_ObjLevel(Hop_Regular(pObjLeft)) != Hop_ObjLevel(Hop_Regular(pObjRight)) )
00289             break;
00290     }
00291     Current++;    
00292     // get the node, for which the equality holds
00293     pObjLeft = Vec_PtrEntry( vSuper, Current );
00294     assert( Hop_ObjLevel(Hop_Regular(pObjLeft)) == Hop_ObjLevel(Hop_Regular(pObjRight)) );
00295     return Current;
00296 }

void Hop_NodeBalancePermute ( Hop_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 310 of file hopBalance.c.

00311 {
00312     Hop_Obj_t * pObj1, * pObj2, * pObj3, * pGhost;
00313     int RightBound, i;
00314     // get the right bound
00315     RightBound = Vec_PtrSize(vSuper) - 2;
00316     assert( LeftBound <= RightBound );
00317     if ( LeftBound == RightBound )
00318         return;
00319     // get the two last nodes
00320     pObj1 = Vec_PtrEntry( vSuper, RightBound + 1 );
00321     pObj2 = Vec_PtrEntry( vSuper, RightBound     );
00322     if ( Hop_Regular(pObj1) == p->pConst1 || Hop_Regular(pObj2) == p->pConst1 )
00323         return;
00324     // find the first node that can be shared
00325     for ( i = RightBound; i >= LeftBound; i-- )
00326     {
00327         pObj3 = Vec_PtrEntry( vSuper, i );
00328         if ( Hop_Regular(pObj3) == p->pConst1 )
00329         {
00330             Vec_PtrWriteEntry( vSuper, i,          pObj2 );
00331             Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
00332             return;
00333         }
00334         pGhost = Hop_ObjCreateGhost( p, pObj1, pObj3, fExor? AIG_EXOR : AIG_AND );
00335         if ( Hop_TableLookup( p, pGhost ) )
00336         {
00337             if ( pObj3 == pObj2 )
00338                 return;
00339             Vec_PtrWriteEntry( vSuper, i,          pObj2 );
00340             Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
00341             return;
00342         }
00343     }
00344 /*
00345     // we did not find the node to share, randomize choice
00346     {
00347         int Choice = rand() % (RightBound - LeftBound + 1);
00348         pObj3 = Vec_PtrEntry( vSuper, LeftBound + Choice );
00349         if ( pObj3 == pObj2 )
00350             return;
00351         Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pObj2 );
00352         Vec_PtrWriteEntry( vSuper, RightBound,         pObj3 );
00353     }
00354 */
00355 }

void Hop_NodeBalancePushUniqueOrderByLevel ( Vec_Ptr_t *  vStore,
Hop_Obj_t *  pObj 
) [static]

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 368 of file hopBalance.c.

00369 {
00370     Hop_Obj_t * pObj1, * pObj2;
00371     int i;
00372     if ( Vec_PtrPushUnique(vStore, pObj) )
00373         return;
00374     // find the p of the node
00375     for ( i = vStore->nSize-1; i > 0; i-- )
00376     {
00377         pObj1 = vStore->pArray[i  ];
00378         pObj2 = vStore->pArray[i-1];
00379         if ( Hop_ObjLevel(Hop_Regular(pObj1)) <= Hop_ObjLevel(Hop_Regular(pObj2)) )
00380             break;
00381         vStore->pArray[i  ] = pObj2;
00382         vStore->pArray[i-1] = pObj1;
00383     }
00384 }

int Hop_NodeCompareLevelsDecrease ( Hop_Obj_t **  pp1,
Hop_Obj_t **  pp2 
)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 214 of file hopBalance.c.

00215 {
00216     int Diff = Hop_ObjLevel(Hop_Regular(*pp1)) - Hop_ObjLevel(Hop_Regular(*pp2));
00217     if ( Diff > 0 )
00218         return -1;
00219     if ( Diff < 0 ) 
00220         return 1;
00221     return 0; 
00222 }

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