diff options
Diffstat (limited to 'src/aig/ivy/ivyBalance.c')
| -rw-r--r-- | src/aig/ivy/ivyBalance.c | 404 |
1 files changed, 0 insertions, 404 deletions
diff --git a/src/aig/ivy/ivyBalance.c b/src/aig/ivy/ivyBalance.c deleted file mode 100644 index 5627039a..00000000 --- a/src/aig/ivy/ivyBalance.c +++ /dev/null @@ -1,404 +0,0 @@ -/**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 $] - -***********************************************************************/ - -#include "ivy.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -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 ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Performs algebraic balancing of the AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel ) -{ - Ivy_Man_t * pNew; - Ivy_Obj_t * pObj, * pDriver; - Vec_Vec_t * vStore; - int i, NewNodeId; - // clean the old manager - Ivy_ManCleanTravId( p ); - // create the new manager - pNew = Ivy_ManStart(); - // map the nodes - Ivy_ManConst1(p)->TravId = Ivy_EdgeFromNode( Ivy_ManConst1(pNew) ); - Ivy_ManForEachPi( p, pObj, i ) - pObj->TravId = Ivy_EdgeFromNode( Ivy_ObjCreatePi(pNew) ); - // if HAIG is defined, trasfer the pointers to the PIs/latches -// if ( p->pHaig ) -// Ivy_ManHaigTrasfer( p, pNew ); - // balance the AIG - vStore = Vec_VecAlloc( 50 ); - Ivy_ManForEachPo( p, pObj, i ) - { - pDriver = Ivy_ObjReal( Ivy_ObjChild0(pObj) ); - NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular(pDriver), vStore, 0, fUpdateLevel ); - NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement(pDriver) ); - Ivy_ObjCreatePo( pNew, Ivy_EdgeToNode(pNew, NewNodeId) ); - } - Vec_VecFree( vStore ); - if ( i = Ivy_ManCleanup( pNew ) ) - { -// printf( "Cleanup after balancing removed %d dangling nodes.\n", i ); - } - // check the resulting AIG - if ( !Ivy_ManCheck(pNew) ) - printf( "Ivy_ManBalance(): The check has failed.\n" ); - return pNew; -} - -/**Function************************************************************* - - Synopsis [Procedure used for sorting the nodes in decreasing order of levels.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_NodeCompareLevelsDecrease( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 ) -{ - int Diff = Ivy_Regular(*pp1)->Level - Ivy_Regular(*pp2)->Level; - if ( Diff > 0 ) - return -1; - if ( Diff < 0 ) - return 1; - return 0; -} - -/**Function************************************************************* - - Synopsis [Returns the ID of new node constructed.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_NodeBalance_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel ) -{ - Ivy_Obj_t * pObjNew; - Vec_Ptr_t * vSuper; - int i, NewNodeId; - assert( !Ivy_IsComplement(pObjOld) ); - assert( !Ivy_ObjIsBuf(pObjOld) ); - // return if the result is known - if ( Ivy_ObjIsConst1(pObjOld) ) - return pObjOld->TravId; - if ( pObjOld->TravId ) - return pObjOld->TravId; - assert( Ivy_ObjIsNode(pObjOld) ); - // get the implication supergate - vSuper = Ivy_NodeBalanceCone( pObjOld, vStore, Level ); - if ( vSuper->nSize == 0 ) - { // it means that the supergate contains two nodes in the opposite polarity - pObjOld->TravId = Ivy_EdgeFromNode( Ivy_ManConst0(pNew) ); - return pObjOld->TravId; - } - if ( vSuper->nSize < 2 ) - printf( "BUG!\n" ); - // for each old node, derive the new well-balanced node - for ( i = 0; i < vSuper->nSize; i++ ) - { - NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel ); - NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement(vSuper->pArray[i]) ); - vSuper->pArray[i] = Ivy_EdgeToNode( pNew, NewNodeId ); - } - // build the supergate - pObjNew = Ivy_NodeBalanceBuildSuper( pNew, vSuper, Ivy_ObjType(pObjOld), fUpdateLevel ); - vSuper->nSize = 0; - // make sure the balanced node is not assigned - assert( pObjOld->TravId == 0 ); - pObjOld->TravId = Ivy_EdgeFromNode( pObjNew ); -// assert( pObjOld->Level >= Ivy_Regular(pObjNew)->Level ); - return pObjOld->TravId; -} - -/**Function************************************************************* - - Synopsis [Builds implication supergate.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Ivy_Man_t * p, Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel ) -{ - Ivy_Obj_t * pObj1, * pObj2; - int LeftBound; - assert( vSuper->nSize > 1 ); - // sort the new nodes by level in the decreasing order - Vec_PtrSort( vSuper, Ivy_NodeCompareLevelsDecrease ); - // balance the nodes - while ( vSuper->nSize > 1 ) - { - // find the left bound on the node to be paired - LeftBound = (!fUpdateLevel)? 0 : Ivy_NodeBalanceFindLeft( vSuper ); - // find the node that can be shared (if no such node, randomize choice) - Ivy_NodeBalancePermute( p, vSuper, LeftBound, Type == IVY_EXOR ); - // pull out the last two nodes - pObj1 = Vec_PtrPop(vSuper); - pObj2 = Vec_PtrPop(vSuper); - Ivy_NodeBalancePushUniqueOrderByLevel( vSuper, Ivy_Oper(p, pObj1, pObj2, Type) ); - } - return Vec_PtrEntry(vSuper, 0); -} - -/**Function************************************************************* - - Synopsis [Collects the nodes of the supergate.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_NodeBalanceCone_rec( Ivy_Obj_t * pRoot, Ivy_Obj_t * pObj, Vec_Ptr_t * vSuper ) -{ - int RetValue1, RetValue2, i; - // check if the node is visited - if ( Ivy_Regular(pObj)->fMarkB ) - { - // check if the node occurs in the same polarity - for ( i = 0; i < vSuper->nSize; i++ ) - if ( vSuper->pArray[i] == pObj ) - return 1; - // check if the node is present in the opposite polarity - for ( i = 0; i < vSuper->nSize; i++ ) - if ( vSuper->pArray[i] == Ivy_Not(pObj) ) - return -1; - assert( 0 ); - return 0; - } - // if the new node is complemented or a PI, another gate begins - if ( pObj != pRoot && (Ivy_IsComplement(pObj) || Ivy_ObjType(pObj) != Ivy_ObjType(pRoot) || Ivy_ObjRefs(pObj) > 1) ) - { - Vec_PtrPush( vSuper, pObj ); - Ivy_Regular(pObj)->fMarkB = 1; - return 0; - } - assert( !Ivy_IsComplement(pObj) ); - assert( Ivy_ObjIsNode(pObj) ); - // go through the branches - RetValue1 = Ivy_NodeBalanceCone_rec( pRoot, Ivy_ObjReal( Ivy_ObjChild0(pObj) ), vSuper ); - RetValue2 = Ivy_NodeBalanceCone_rec( pRoot, Ivy_ObjReal( Ivy_ObjChild1(pObj) ), vSuper ); - if ( RetValue1 == -1 || RetValue2 == -1 ) - return -1; - // return 1 if at least one branch has a duplicate - return RetValue1 || RetValue2; -} - -/**Function************************************************************* - - Synopsis [Collects the nodes of the supergate.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Ivy_NodeBalanceCone( Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level ) -{ - Vec_Ptr_t * vNodes; - int RetValue, i; - assert( !Ivy_IsComplement(pObj) ); - // extend the storage - if ( Vec_VecSize( vStore ) <= Level ) - Vec_VecPush( vStore, Level, 0 ); - // get the temporary array of nodes - vNodes = Vec_VecEntry( vStore, Level ); - Vec_PtrClear( vNodes ); - // collect the nodes in the implication supergate - RetValue = Ivy_NodeBalanceCone_rec( pObj, pObj, vNodes ); - assert( vNodes->nSize > 1 ); - // unmark the visited nodes - Vec_PtrForEachEntry( vNodes, pObj, i ) - Ivy_Regular(pObj)->fMarkB = 0; - // if we found the node and its complement in the same implication supergate, - // return empty set of nodes (meaning that we should use constant-0 node) - if ( RetValue == -1 ) - vNodes->nSize = 0; - return vNodes; -} - -/**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 [] - -***********************************************************************/ -int Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper ) -{ - Ivy_Obj_t * pObjRight, * pObjLeft; - int Current; - // if two or less nodes, pair with the first - if ( Vec_PtrSize(vSuper) < 3 ) - return 0; - // set the pointer to the one before the last - Current = Vec_PtrSize(vSuper) - 2; - pObjRight = Vec_PtrEntry( vSuper, Current ); - // go through the nodes to the left of this one - for ( Current--; Current >= 0; Current-- ) - { - // get the next node on the left - pObjLeft = Vec_PtrEntry( vSuper, Current ); - // if the level of this node is different, quit the loop - if ( Ivy_Regular(pObjLeft)->Level != Ivy_Regular(pObjRight)->Level ) - break; - } - Current++; - // get the node, for which the equality holds - pObjLeft = Vec_PtrEntry( vSuper, Current ); - assert( Ivy_Regular(pObjLeft)->Level == Ivy_Regular(pObjRight)->Level ); - return Current; -} - -/**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 [] - -***********************************************************************/ -void Ivy_NodeBalancePermute( Ivy_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor ) -{ - Ivy_Obj_t * pObj1, * pObj2, * pObj3, * pGhost; - int RightBound, i; - // get the right bound - RightBound = Vec_PtrSize(vSuper) - 2; - assert( LeftBound <= RightBound ); - if ( LeftBound == RightBound ) - return; - // get the two last nodes - pObj1 = Vec_PtrEntry( vSuper, RightBound + 1 ); - pObj2 = Vec_PtrEntry( vSuper, RightBound ); - if ( Ivy_Regular(pObj1) == p->pConst1 || Ivy_Regular(pObj2) == p->pConst1 ) - return; - // find the first node that can be shared - for ( i = RightBound; i >= LeftBound; i-- ) - { - pObj3 = Vec_PtrEntry( vSuper, i ); - if ( Ivy_Regular(pObj3) == p->pConst1 ) - { - Vec_PtrWriteEntry( vSuper, i, pObj2 ); - Vec_PtrWriteEntry( vSuper, RightBound, pObj3 ); - return; - } - pGhost = Ivy_ObjCreateGhost( p, pObj1, pObj3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE ); - if ( Ivy_TableLookup( p, pGhost ) ) - { - if ( pObj3 == pObj2 ) - return; - Vec_PtrWriteEntry( vSuper, i, pObj2 ); - Vec_PtrWriteEntry( vSuper, RightBound, pObj3 ); - return; - } - } -/* - // we did not find the node to share, randomize choice - { - int Choice = rand() % (RightBound - LeftBound + 1); - pObj3 = Vec_PtrEntry( vSuper, LeftBound + Choice ); - if ( pObj3 == pObj2 ) - return; - Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pObj2 ); - Vec_PtrWriteEntry( vSuper, RightBound, pObj3 ); - } -*/ -} - -/**Function************************************************************* - - Synopsis [Inserts a new node in the order by levels.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Ivy_Obj_t * pObj ) -{ - Ivy_Obj_t * pObj1, * pObj2; - int i; - if ( Vec_PtrPushUnique(vStore, pObj) ) - return; - // find the p of the node - for ( i = vStore->nSize-1; i > 0; i-- ) - { - pObj1 = vStore->pArray[i ]; - pObj2 = vStore->pArray[i-1]; - if ( Ivy_Regular(pObj1)->Level <= Ivy_Regular(pObj2)->Level ) - break; - vStore->pArray[i ] = pObj2; - vStore->pArray[i-1] = pObj1; - } -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |