| /**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 $] |
| |
| ***********************************************************************/ |
| |
| #include "darInt.h" |
| #include "misc/tim/tim.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //#define USE_LUTSIZE_BALANCE |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Uniqifies the node.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Dar_ObjCompareLits( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 ) |
| { |
| int Diff = Aig_ObjToLit(*pp1) - Aig_ObjToLit(*pp2); |
| if ( Diff < 0 ) |
| return -1; |
| if ( Diff > 0 ) |
| return 1; |
| return 0; |
| } |
| void Dar_BalanceUniqify( Aig_Obj_t * pObj, Vec_Ptr_t * vNodes, int fExor ) |
| { |
| Aig_Obj_t * pTemp, * pTempNext; |
| int i, k; |
| // sort the nodes by their literal |
| Vec_PtrSort( vNodes, (int (*)())Dar_ObjCompareLits ); |
| // remove duplicates |
| k = 0; |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pTemp, i ) |
| { |
| if ( i + 1 == Vec_PtrSize(vNodes) ) |
| { |
| Vec_PtrWriteEntry( vNodes, k++, pTemp ); |
| break; |
| } |
| pTempNext = (Aig_Obj_t *)Vec_PtrEntry( vNodes, i+1 ); |
| if ( !fExor && pTemp == Aig_Not(pTempNext) ) // pos_lit & neg_lit = 0 |
| { |
| Vec_PtrClear( vNodes ); |
| return; |
| } |
| if ( pTemp != pTempNext ) // save if different |
| Vec_PtrWriteEntry( vNodes, k++, pTemp ); |
| else if ( fExor ) // in case of XOR, remove identical |
| i++; |
| } |
| Vec_PtrShrink( vNodes, k ); |
| if ( Vec_PtrSize(vNodes) < 2 ) |
| return; |
| // check that there is no duplicates |
| pTemp = (Aig_Obj_t *)Vec_PtrEntry( vNodes, 0 ); |
| Vec_PtrForEachEntryStart( Aig_Obj_t *, vNodes, pTempNext, i, 1 ) |
| { |
| assert( pTemp != pTempNext ); |
| pTemp = pTempNext; |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collects the nodes of the supergate.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper ) |
| { |
| if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1 || Vec_PtrSize(vSuper) > 10000) ) |
| Vec_PtrPush( vSuper, pObj ); |
| else |
| { |
| assert( !Aig_IsComplement(pObj) ); |
| assert( Aig_ObjIsNode(pObj) ); |
| // go through the branches |
| Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper ); |
| Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper ); |
| } |
| } |
| Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level ) |
| { |
| Vec_Ptr_t * vNodes; |
| assert( !Aig_IsComplement(pObj) ); |
| assert( Aig_ObjIsNode(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 |
| Dar_BalanceCone_rec( pObj, pObj, vNodes ); |
| // remove duplicates |
| Dar_BalanceUniqify( pObj, vNodes, Aig_ObjIsExor(pObj) ); |
| return vNodes; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collects the nodes of the supergate.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| /* |
| int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper ) |
| { |
| int RetValue1, RetValue2, i; |
| // check if the node is visited |
| if ( Aig_Regular(pObj)->fMarkB ) |
| { |
| if ( Aig_ObjIsExor(pRoot) ) |
| { |
| assert( !Aig_IsComplement(pObj) ); |
| // check if the node occurs in the same polarity |
| Vec_PtrRemove( vSuper, pObj ); |
| Aig_Regular(pObj)->fMarkB = 0; |
| //printf( " Duplicated EXOR input!!! " ); |
| return 1; |
| } |
| else |
| { |
| // 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] == Aig_Not(pObj) ) |
| return -1; |
| } |
| assert( 0 ); |
| return 0; |
| } |
| // if the new node is complemented or a PI, another gate begins |
| if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1 || Vec_PtrSize(vSuper) > 10000) ) |
| { |
| Vec_PtrPush( vSuper, pObj ); |
| Aig_Regular(pObj)->fMarkB = 1; |
| return 0; |
| } |
| assert( !Aig_IsComplement(pObj) ); |
| assert( Aig_ObjIsNode(pObj) ); |
| // go through the branches |
| RetValue1 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper ); |
| RetValue2 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper ); |
| if ( RetValue1 == -1 || RetValue2 == -1 ) |
| return -1; |
| // return 1 if at least one branch has a duplicate |
| return RetValue1 || RetValue2; |
| } |
| Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level ) |
| { |
| Vec_Ptr_t * vNodes; |
| int RetValue, i; |
| assert( !Aig_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 = Dar_BalanceCone_rec( pObj, pObj, vNodes ); |
| assert( RetValue != 0 || vNodes->nSize > 1 ); |
| // unmark the visited nodes |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) |
| Aig_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 Dar_BalanceFindLeft( Vec_Ptr_t * vSuper ) |
| { |
| Aig_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 = (Aig_Obj_t *)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 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, Current ); |
| // if the level of this node is different, quit the loop |
| if ( Aig_ObjLevel(Aig_Regular(pObjLeft)) != Aig_ObjLevel(Aig_Regular(pObjRight)) ) |
| break; |
| } |
| Current++; |
| // get the node, for which the equality holds |
| pObjLeft = (Aig_Obj_t *)Vec_PtrEntry( vSuper, Current ); |
| assert( Aig_ObjLevel(Aig_Regular(pObjLeft)) == Aig_ObjLevel(Aig_Regular(pObjRight)) ); |
| 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 Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor ) |
| { |
| Aig_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 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, RightBound + 1 ); |
| pObj2 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, RightBound ); |
| if ( Aig_Regular(pObj1) == p->pConst1 || Aig_Regular(pObj2) == p->pConst1 || Aig_Regular(pObj1) == Aig_Regular(pObj2) ) |
| return; |
| // find the first node that can be shared |
| for ( i = RightBound; i >= LeftBound; i-- ) |
| { |
| pObj3 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, i ); |
| if ( Aig_Regular(pObj3) == p->pConst1 ) |
| { |
| Vec_PtrWriteEntry( vSuper, i, pObj2 ); |
| Vec_PtrWriteEntry( vSuper, RightBound, pObj3 ); |
| return; |
| } |
| if ( Aig_Regular(pObj1) == Aig_Regular(pObj3) ) |
| { |
| if ( pObj3 == pObj2 ) |
| return; |
| Vec_PtrWriteEntry( vSuper, i, pObj2 ); |
| Vec_PtrWriteEntry( vSuper, RightBound, pObj3 ); |
| return; |
| } |
| pGhost = Aig_ObjCreateGhost( p, pObj1, pObj3, fExor? AIG_OBJ_EXOR : AIG_OBJ_AND ); |
| if ( Aig_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 = Aig_ManRandom(0) % (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 [Procedure used for sorting the nodes in decreasing order of levels.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Aig_NodeCompareLevelsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 ) |
| { |
| int Diff = Aig_ObjLevel(Aig_Regular(*pp1)) - Aig_ObjLevel(Aig_Regular(*pp2)); |
| if ( Diff > 0 ) |
| return -1; |
| if ( Diff < 0 ) |
| return 1; |
| Diff = Aig_ObjId(Aig_Regular(*pp1)) - Aig_ObjId(Aig_Regular(*pp2)); |
| if ( Diff > 0 ) |
| return -1; |
| if ( Diff < 0 ) |
| return 1; |
| return 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Inserts a new node in the order by levels.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj, int fExor ) |
| { |
| Aig_Obj_t * pObj1, * pObj2; |
| int i; |
| if ( Vec_PtrPushUnique(vStore, pObj) ) |
| { |
| if ( fExor ) |
| Vec_PtrRemove(vStore, pObj); |
| return; |
| } |
| // find the p of the node |
| for ( i = vStore->nSize-1; i > 0; i-- ) |
| { |
| pObj1 = (Aig_Obj_t *)vStore->pArray[i ]; |
| pObj2 = (Aig_Obj_t *)vStore->pArray[i-1]; |
| if ( Aig_ObjLevel(Aig_Regular(pObj1)) <= Aig_ObjLevel(Aig_Regular(pObj2)) ) |
| break; |
| vStore->pArray[i ] = pObj2; |
| vStore->pArray[i-1] = pObj1; |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Builds implication supergate.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel ) |
| { |
| Aig_Obj_t * pObj1, * pObj2; |
| int LeftBound; |
| assert( vSuper->nSize > 1 ); |
| // sort the new nodes by level in the decreasing order |
| Vec_PtrSort( vSuper, (int (*)(void))Aig_NodeCompareLevelsDecrease ); |
| // balance the nodes |
| while ( vSuper->nSize > 1 ) |
| { |
| // find the left bound on the node to be paired |
| LeftBound = (!fUpdateLevel)? 0 : Dar_BalanceFindLeft( vSuper ); |
| // find the node that can be shared (if no such node, randomize choice) |
| Dar_BalancePermute( p, vSuper, LeftBound, Type == AIG_OBJ_EXOR ); |
| // pull out the last two nodes |
| pObj1 = (Aig_Obj_t *)Vec_PtrPop(vSuper); |
| pObj2 = (Aig_Obj_t *)Vec_PtrPop(vSuper); |
| Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type), Type == AIG_OBJ_EXOR ); |
| } |
| return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns affective support size.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Aig_BaseSize( Aig_Man_t * p, Aig_Obj_t * pObj, int nLutSize ) |
| { |
| int nBaseSize; |
| pObj = Aig_Regular(pObj); |
| if ( Aig_ObjIsConst1(pObj) ) |
| return 0; |
| if ( Aig_ObjLevel(pObj) >= nLutSize ) |
| return 1; |
| nBaseSize = Aig_SupportSize( p, pObj ); |
| if ( nBaseSize >= nLutSize ) |
| return 1; |
| return nBaseSize; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Builds implication supergate.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Obj_t * Dar_BalanceBuildSuperTop( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel, int nLutSize ) |
| { |
| Vec_Ptr_t * vSubset; |
| Aig_Obj_t * pObj; |
| int i, nBaseSizeAll, nBaseSize; |
| assert( vSuper->nSize > 1 ); |
| // sort the new nodes by level in the decreasing order |
| Vec_PtrSort( vSuper, (int (*)(void))Aig_NodeCompareLevelsDecrease ); |
| // add one LUT at a time |
| while ( Vec_PtrSize(vSuper) > 1 ) |
| { |
| // isolate the group of nodes with nLutSize inputs |
| nBaseSizeAll = 0; |
| vSubset = Vec_PtrAlloc( nLutSize ); |
| Vec_PtrForEachEntryReverse( Aig_Obj_t *, vSuper, pObj, i ) |
| { |
| nBaseSize = Aig_BaseSize( p, pObj, nLutSize ); |
| if ( nBaseSizeAll + nBaseSize > nLutSize && Vec_PtrSize(vSubset) > 1 ) |
| break; |
| nBaseSizeAll += nBaseSize; |
| Vec_PtrPush( vSubset, pObj ); |
| } |
| // remove them from vSuper |
| Vec_PtrShrink( vSuper, Vec_PtrSize(vSuper) - Vec_PtrSize(vSubset) ); |
| // create the new supergate |
| pObj = Dar_BalanceBuildSuper( p, vSubset, Type, fUpdateLevel ); |
| Vec_PtrFree( vSubset ); |
| // add the new output |
| Dar_BalancePushUniqueOrderByLevel( vSuper, pObj, Type == AIG_OBJ_EXOR ); |
| } |
| return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the new node constructed.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel ) |
| { |
| Aig_Obj_t * pObjNew; |
| Vec_Ptr_t * vSuper; |
| int i; |
| assert( !Aig_IsComplement(pObjOld) ); |
| assert( !Aig_ObjIsBuf(pObjOld) ); |
| // return if the result is known |
| if ( pObjOld->pData ) |
| return (Aig_Obj_t *)pObjOld->pData; |
| assert( Aig_ObjIsNode(pObjOld) ); |
| // get the implication supergate |
| vSuper = Dar_BalanceCone( pObjOld, vStore, Level ); |
| // check if supergate contains two nodes in the opposite polarity |
| if ( vSuper->nSize == 0 ) |
| return (Aig_Obj_t *)(pObjOld->pData = Aig_ManConst0(pNew)); |
| // for each old node, derive the new well-balanced node |
| for ( i = 0; i < Vec_PtrSize(vSuper); i++ ) |
| { |
| pObjNew = Dar_Balance_rec( pNew, Aig_Regular((Aig_Obj_t *)vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel ); |
| if ( pObjNew == NULL ) |
| return NULL; |
| vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement((Aig_Obj_t *)vSuper->pArray[i]) ); |
| } |
| // check for exactly one node |
| if ( vSuper->nSize == 1 ) |
| return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0); |
| // build the supergate |
| #ifdef USE_LUTSIZE_BALANCE |
| pObjNew = Dar_BalanceBuildSuperTop( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel, 6 ); |
| #else |
| pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel ); |
| #endif |
| if ( pNew->Time2Quit && !(Aig_Regular(pObjNew)->Id & 255) && Abc_Clock() > pNew->Time2Quit ) |
| return NULL; |
| // make sure the balanced node is not assigned |
| // assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level ); |
| assert( pObjOld->pData == NULL ); |
| return (Aig_Obj_t *)(pObjOld->pData = pObjNew); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs algebraic balancing of the AIG.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) |
| { |
| Aig_Man_t * pNew; |
| Aig_Obj_t * pObj, * pDriver, * pObjNew; |
| Vec_Vec_t * vStore; |
| int i; |
| assert( Aig_ManVerifyTopoOrder(p) ); |
| // create the new manager |
| pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| pNew->nAsserts = p->nAsserts; |
| pNew->nConstrs = p->nConstrs; |
| pNew->nBarBufs = p->nBarBufs; |
| pNew->Time2Quit = p->Time2Quit; |
| if ( p->vFlopNums ) |
| pNew->vFlopNums = Vec_IntDup( p->vFlopNums ); |
| // map the PI nodes |
| Aig_ManCleanData( p ); |
| Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); |
| vStore = Vec_VecAlloc( 50 ); |
| if ( p->pManTime != NULL ) |
| { |
| float arrTime; |
| Tim_ManIncrementTravId( (Tim_Man_t *)p->pManTime ); |
| Aig_ManSetCioIds( p ); |
| Aig_ManForEachObj( p, pObj, i ) |
| { |
| if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) ) |
| continue; |
| if ( Aig_ObjIsCi(pObj) ) |
| { |
| // copy the PI |
| pObjNew = Aig_ObjCreateCi(pNew); |
| pObj->pData = pObjNew; |
| // set the arrival time of the new PI |
| arrTime = Tim_ManGetCiArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) ); |
| pObjNew->Level = (int)arrTime; |
| } |
| else if ( Aig_ObjIsCo(pObj) ) |
| { |
| // perform balancing |
| pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); |
| pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel ); |
| if ( pObjNew == NULL ) |
| { |
| Vec_VecFree( vStore ); |
| Aig_ManStop( pNew ); |
| return NULL; |
| } |
| pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) ); |
| // save arrival time of the output |
| arrTime = (float)Aig_Regular(pObjNew)->Level; |
| Tim_ManSetCoArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj), arrTime ); |
| // create PO |
| pObjNew = Aig_ObjCreateCo( pNew, pObjNew ); |
| } |
| else |
| assert( 0 ); |
| } |
| Aig_ManCleanCioIds( p ); |
| pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 ); |
| } |
| else |
| { |
| Aig_ManForEachCi( p, pObj, i ) |
| { |
| pObjNew = Aig_ObjCreateCi(pNew); |
| pObjNew->Level = pObj->Level; |
| pObj->pData = pObjNew; |
| } |
| if ( p->nBarBufs == 0 ) |
| { |
| Aig_ManForEachCo( p, pObj, i ) |
| { |
| pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); |
| pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel ); |
| if ( pObjNew == NULL ) |
| { |
| Vec_VecFree( vStore ); |
| Aig_ManStop( pNew ); |
| return NULL; |
| } |
| pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) ); |
| pObjNew = Aig_ObjCreateCo( pNew, pObjNew ); |
| } |
| } |
| else |
| { |
| Vec_Ptr_t * vLits = Vec_PtrStart( Aig_ManCoNum(p) ); |
| Aig_ManForEachCo( p, pObj, i ) |
| { |
| int k = i < p->nBarBufs ? Aig_ManCoNum(p) - p->nBarBufs + i : i - p->nBarBufs; |
| pObj = Aig_ManCo( p, k ); |
| pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); |
| pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel ); |
| if ( pObjNew == NULL ) |
| { |
| Vec_VecFree( vStore ); |
| Aig_ManStop( pNew ); |
| return NULL; |
| } |
| pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) ); |
| Vec_PtrWriteEntry( vLits, k, pObjNew ); |
| if ( i < p->nBarBufs ) |
| Aig_ManCi(pNew, Aig_ManCiNum(p) - p->nBarBufs + i)->Level = Aig_Regular(pObjNew)->Level; |
| } |
| Aig_ManForEachCo( p, pObj, i ) |
| Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vLits, i) ); |
| Vec_PtrFree(vLits); |
| } |
| } |
| Vec_VecFree( vStore ); |
| // remove dangling nodes |
| Aig_ManCleanup( pNew ); |
| Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) ); |
| // check the resulting AIG |
| if ( !Aig_ManCheck(pNew) ) |
| printf( "Dar_ManBalance(): The check has failed.\n" ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reproduces script "compress2".] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose ) |
| { |
| Aig_Man_t * pAigXor, * pRes; |
| if ( fExor ) |
| { |
| pAigXor = Aig_ManDupExor( pAig ); |
| if ( fVerbose ) |
| Dar_BalancePrintStats( pAigXor ); |
| pRes = Dar_ManBalance( pAigXor, fUpdateLevel ); |
| Aig_ManStop( pAigXor ); |
| } |
| else |
| { |
| pRes = Dar_ManBalance( pAig, fUpdateLevel ); |
| } |
| return pRes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Inserts a new node in the order by levels.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Dar_BalancePrintStats( Aig_Man_t * p ) |
| { |
| Vec_Ptr_t * vSuper; |
| Aig_Obj_t * pObj, * pTemp; |
| int i, k; |
| if ( Aig_ManExorNum(p) == 0 ) |
| { |
| printf( "There is no EXOR gates.\n" ); |
| return; |
| } |
| Aig_ManForEachExor( p, pObj, i ) |
| { |
| Aig_ObjFanin0(pObj)->fMarkA = 1; |
| Aig_ObjFanin1(pObj)->fMarkA = 1; |
| assert( !Aig_ObjFaninC0(pObj) ); |
| assert( !Aig_ObjFaninC1(pObj) ); |
| } |
| vSuper = Vec_PtrAlloc( 1000 ); |
| Aig_ManForEachExor( p, pObj, i ) |
| { |
| if ( pObj->fMarkA && pObj->nRefs == 1 ) |
| continue; |
| Vec_PtrClear( vSuper ); |
| Dar_BalanceCone_rec( pObj, pObj, vSuper ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pTemp, k ) |
| pTemp->fMarkB = 0; |
| if ( Vec_PtrSize(vSuper) < 3 ) |
| continue; |
| printf( " %d(", Vec_PtrSize(vSuper) ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pTemp, k ) |
| printf( " %d", pTemp->Level ); |
| printf( " )" ); |
| } |
| Vec_PtrFree( vSuper ); |
| Aig_ManForEachObj( p, pObj, i ) |
| pObj->fMarkA = 0; |
| printf( "\n" ); |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
