src/aig/ivy/ivyBalance.c File Reference

#include "ivy.h"
Include dependency graph for ivyBalance.c:

Go to the source code of this file.

Functions

static int Ivy_NodeBalance_rec (Ivy_Man_t *pNew, Ivy_Obj_t *pObj, Vec_Vec_t *vStore, int Level, int fUpdateLevel)
static Vec_Ptr_t * Ivy_NodeBalanceCone (Ivy_Obj_t *pObj, Vec_Vec_t *vStore, int Level)
static int Ivy_NodeBalanceFindLeft (Vec_Ptr_t *vSuper)
static void Ivy_NodeBalancePermute (Ivy_Man_t *p, Vec_Ptr_t *vSuper, int LeftBound, int fExor)
static void Ivy_NodeBalancePushUniqueOrderByLevel (Vec_Ptr_t *vStore, Ivy_Obj_t *pObj)
Ivy_Man_t * Ivy_ManBalance (Ivy_Man_t *p, int fUpdateLevel)
int Ivy_NodeCompareLevelsDecrease (Ivy_Obj_t **pp1, Ivy_Obj_t **pp2)
Ivy_Obj_t * Ivy_NodeBalanceBuildSuper (Ivy_Man_t *p, Vec_Ptr_t *vSuper, Ivy_Type_t Type, int fUpdateLevel)
int Ivy_NodeBalanceCone_rec (Ivy_Obj_t *pRoot, Ivy_Obj_t *pObj, Vec_Ptr_t *vSuper)

Function Documentation

Ivy_Man_t* Ivy_ManBalance ( Ivy_Man_t *  p,
int  fUpdateLevel 
)

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

Synopsis [Performs algebraic balancing of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file ivyBalance.c.

00049 {
00050     Ivy_Man_t * pNew;
00051     Ivy_Obj_t * pObj, * pDriver;
00052     Vec_Vec_t * vStore;
00053     int i, NewNodeId;
00054     // clean the old manager
00055     Ivy_ManCleanTravId( p );
00056     // create the new manager 
00057     pNew = Ivy_ManStart();
00058     // map the nodes
00059     Ivy_ManConst1(p)->TravId = Ivy_EdgeFromNode( Ivy_ManConst1(pNew) );
00060     Ivy_ManForEachPi( p, pObj, i )
00061         pObj->TravId = Ivy_EdgeFromNode( Ivy_ObjCreatePi(pNew) );
00062     // if HAIG is defined, trasfer the pointers to the PIs/latches
00063 //    if ( p->pHaig )
00064 //        Ivy_ManHaigTrasfer( p, pNew );
00065     // balance the AIG
00066     vStore = Vec_VecAlloc( 50 );
00067     Ivy_ManForEachPo( p, pObj, i )
00068     {
00069         pDriver   = Ivy_ObjReal( Ivy_ObjChild0(pObj) );
00070         NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular(pDriver), vStore, 0, fUpdateLevel );
00071         NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement(pDriver) );
00072         Ivy_ObjCreatePo( pNew, Ivy_EdgeToNode(pNew, NewNodeId) );
00073     }
00074     Vec_VecFree( vStore );
00075     if ( i = Ivy_ManCleanup( pNew ) )
00076     {
00077 //        printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
00078     }
00079     // check the resulting AIG
00080     if ( !Ivy_ManCheck(pNew) )
00081         printf( "Ivy_ManBalance(): The check has failed.\n" );
00082     return pNew;
00083 }

int Ivy_NodeBalance_rec ( Ivy_Man_t *  pNew,
Ivy_Obj_t *  pObjOld,
Vec_Vec_t *  vStore,
int  Level,
int  fUpdateLevel 
) [static]

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

FileName [ivyBalance.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis [Algebraic AIG balancing.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

] DECLARATIONS ///

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

Synopsis [Returns the ID of new node constructed.]

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file ivyBalance.c.

00118 {
00119     Ivy_Obj_t * pObjNew;
00120     Vec_Ptr_t * vSuper;
00121     int i, NewNodeId;
00122     assert( !Ivy_IsComplement(pObjOld) );
00123     assert( !Ivy_ObjIsBuf(pObjOld) );
00124     // return if the result is known
00125     if ( Ivy_ObjIsConst1(pObjOld) )
00126         return pObjOld->TravId;
00127     if ( pObjOld->TravId )
00128         return pObjOld->TravId;
00129     assert( Ivy_ObjIsNode(pObjOld) );
00130     // get the implication supergate
00131     vSuper = Ivy_NodeBalanceCone( pObjOld, vStore, Level );
00132     if ( vSuper->nSize == 0 )
00133     { // it means that the supergate contains two nodes in the opposite polarity
00134         pObjOld->TravId = Ivy_EdgeFromNode( Ivy_ManConst0(pNew) );
00135         return pObjOld->TravId;
00136     }
00137     if ( vSuper->nSize < 2 )
00138         printf( "BUG!\n" );
00139     // for each old node, derive the new well-balanced node
00140     for ( i = 0; i < vSuper->nSize; i++ )
00141     {
00142         NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
00143         NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement(vSuper->pArray[i]) );
00144         vSuper->pArray[i] = Ivy_EdgeToNode( pNew, NewNodeId );
00145     }
00146     // build the supergate
00147     pObjNew = Ivy_NodeBalanceBuildSuper( pNew, vSuper, Ivy_ObjType(pObjOld), fUpdateLevel );
00148     vSuper->nSize = 0;
00149     // make sure the balanced node is not assigned
00150     assert( pObjOld->TravId == 0 );
00151     pObjOld->TravId = Ivy_EdgeFromNode( pObjNew );
00152 //    assert( pObjOld->Level >= Ivy_Regular(pObjNew)->Level );
00153     return pObjOld->TravId;
00154 }

Ivy_Obj_t* Ivy_NodeBalanceBuildSuper ( Ivy_Man_t *  p,
Vec_Ptr_t *  vSuper,
Ivy_Type_t  Type,
int  fUpdateLevel 
)

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

Synopsis [Builds implication supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 167 of file ivyBalance.c.

00168 {
00169     Ivy_Obj_t * pObj1, * pObj2;
00170     int LeftBound;
00171     assert( vSuper->nSize > 1 );
00172     // sort the new nodes by level in the decreasing order
00173     Vec_PtrSort( vSuper, Ivy_NodeCompareLevelsDecrease );
00174     // balance the nodes
00175     while ( vSuper->nSize > 1 )
00176     {
00177         // find the left bound on the node to be paired
00178         LeftBound = (!fUpdateLevel)? 0 : Ivy_NodeBalanceFindLeft( vSuper );
00179         // find the node that can be shared (if no such node, randomize choice)
00180         Ivy_NodeBalancePermute( p, vSuper, LeftBound, Type == IVY_EXOR );
00181         // pull out the last two nodes
00182         pObj1 = Vec_PtrPop(vSuper);
00183         pObj2 = Vec_PtrPop(vSuper);
00184         Ivy_NodeBalancePushUniqueOrderByLevel( vSuper, Ivy_Oper(p, pObj1, pObj2, Type) );
00185     }
00186     return Vec_PtrEntry(vSuper, 0);
00187 }

Vec_Ptr_t * Ivy_NodeBalanceCone ( Ivy_Obj_t *  pObj,
Vec_Vec_t *  vStore,
int  Level 
) [static]

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

Synopsis [Collects the nodes of the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 246 of file ivyBalance.c.

00247 {
00248     Vec_Ptr_t * vNodes;
00249     int RetValue, i;
00250     assert( !Ivy_IsComplement(pObj) );
00251     // extend the storage
00252     if ( Vec_VecSize( vStore ) <= Level )
00253         Vec_VecPush( vStore, Level, 0 );
00254     // get the temporary array of nodes
00255     vNodes = Vec_VecEntry( vStore, Level );
00256     Vec_PtrClear( vNodes );
00257     // collect the nodes in the implication supergate
00258     RetValue = Ivy_NodeBalanceCone_rec( pObj, pObj, vNodes );
00259     assert( vNodes->nSize > 1 );
00260     // unmark the visited nodes
00261     Vec_PtrForEachEntry( vNodes, pObj, i )
00262         Ivy_Regular(pObj)->fMarkB = 0;
00263     // if we found the node and its complement in the same implication supergate, 
00264     // return empty set of nodes (meaning that we should use constant-0 node)
00265     if ( RetValue == -1 )
00266         vNodes->nSize = 0;
00267     return vNodes;
00268 }

int Ivy_NodeBalanceCone_rec ( Ivy_Obj_t *  pRoot,
Ivy_Obj_t *  pObj,
Vec_Ptr_t *  vSuper 
)

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

Synopsis [Collects the nodes of the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 200 of file ivyBalance.c.

00201 {
00202     int RetValue1, RetValue2, i;
00203     // check if the node is visited
00204     if ( Ivy_Regular(pObj)->fMarkB )
00205     {
00206         // check if the node occurs in the same polarity
00207         for ( i = 0; i < vSuper->nSize; i++ )
00208             if ( vSuper->pArray[i] == pObj )
00209                 return 1;
00210         // check if the node is present in the opposite polarity
00211         for ( i = 0; i < vSuper->nSize; i++ )
00212             if ( vSuper->pArray[i] == Ivy_Not(pObj) )
00213                 return -1;
00214         assert( 0 );
00215         return 0;
00216     }
00217     // if the new node is complemented or a PI, another gate begins
00218     if ( pObj != pRoot && (Ivy_IsComplement(pObj) || Ivy_ObjType(pObj) != Ivy_ObjType(pRoot) || Ivy_ObjRefs(pObj) > 1) )
00219     {
00220         Vec_PtrPush( vSuper, pObj );
00221         Ivy_Regular(pObj)->fMarkB = 1;
00222         return 0;
00223     }
00224     assert( !Ivy_IsComplement(pObj) );
00225     assert( Ivy_ObjIsNode(pObj) );
00226     // go through the branches
00227     RetValue1 = Ivy_NodeBalanceCone_rec( pRoot, Ivy_ObjReal( Ivy_ObjChild0(pObj) ), vSuper );
00228     RetValue2 = Ivy_NodeBalanceCone_rec( pRoot, Ivy_ObjReal( Ivy_ObjChild1(pObj) ), vSuper );
00229     if ( RetValue1 == -1 || RetValue2 == -1 )
00230         return -1;
00231     // return 1 if at least one branch has a duplicate
00232     return RetValue1 || RetValue2;
00233 }

int Ivy_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 285 of file ivyBalance.c.

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

void Ivy_NodeBalancePermute ( Ivy_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 323 of file ivyBalance.c.

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

void Ivy_NodeBalancePushUniqueOrderByLevel ( Vec_Ptr_t *  vStore,
Ivy_Obj_t *  pObj 
) [static]

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 381 of file ivyBalance.c.

00382 {
00383     Ivy_Obj_t * pObj1, * pObj2;
00384     int i;
00385     if ( Vec_PtrPushUnique(vStore, pObj) )
00386         return;
00387     // find the p of the node
00388     for ( i = vStore->nSize-1; i > 0; i-- )
00389     {
00390         pObj1 = vStore->pArray[i  ];
00391         pObj2 = vStore->pArray[i-1];
00392         if ( Ivy_Regular(pObj1)->Level <= Ivy_Regular(pObj2)->Level )
00393             break;
00394         vStore->pArray[i  ] = pObj2;
00395         vStore->pArray[i-1] = pObj1;
00396     }
00397 }

int Ivy_NodeCompareLevelsDecrease ( Ivy_Obj_t **  pp1,
Ivy_Obj_t **  pp2 
)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 96 of file ivyBalance.c.

00097 {
00098     int Diff = Ivy_Regular(*pp1)->Level - Ivy_Regular(*pp2)->Level;
00099     if ( Diff > 0 )
00100         return -1;
00101     if ( Diff < 0 ) 
00102         return 1;
00103     return 0; 
00104 }

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