diff options
Diffstat (limited to 'src/opt/dar/darBalance.c')
| -rw-r--r-- | src/opt/dar/darBalance.c | 645 |
1 files changed, 645 insertions, 0 deletions
diff --git a/src/opt/dar/darBalance.c b/src/opt/dar/darBalance.c new file mode 100644 index 00000000..56ec51fa --- /dev/null +++ b/src/opt/dar/darBalance.c @@ -0,0 +1,645 @@ +/**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 "src/misc/tim/tim.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//#define USE_LUTSIZE_BALANCE + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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; +} + +/**Function************************************************************* + + Synopsis [Collects the nodes of the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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 ) +{ + Aig_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 = (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) ); + } + 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 ); + } + 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)); + if ( vSuper->nSize == 1 ) + return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0); + if ( Vec_PtrSize(vSuper) < 2 ) + printf( "Dar_Balance_rec: Internal error!\n" ); + // 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 ); + vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement((Aig_Obj_t *)vSuper->pArray[i]) ); + } + // 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 + // make sure the balanced node is not assigned +// assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level ); + assert( pObjOld->pData == NULL ); + if ( pNew->pManHaig != NULL ) + { + Aig_Obj_t * pObjNewR = Aig_Regular(pObjNew); +// printf( "Balancing HAIG node %d equivalent to HAIG node %d (over = %d).\n", +// pObjNewR->pHaig->Id, pObjOld->pHaig->Id, pObjNewR->pHaig->pHaig != NULL ); + assert( pObjNewR->pHaig != NULL ); + assert( !Aig_IsComplement(pObjNewR->pHaig) ); + assert( pNew->pManHaig->vEquPairs != NULL ); + Vec_IntPush( pNew->pManHaig->vEquPairs, pObjNewR->pHaig->Id ); + Vec_IntPush( pNew->pManHaig->vEquPairs, pObjOld->pHaig->Id ); + } + else + Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig; + 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; + if ( p->vFlopNums ) + pNew->vFlopNums = Vec_IntDup( p->vFlopNums ); + // pass the HAIG manager + if ( p->pManHaig != NULL ) + { + pNew->pManHaig = p->pManHaig; p->pManHaig = NULL; + Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(pNew->pManHaig); + } + // 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_ManSetPioNumbers( p ); + Aig_ManForEachObj( p, pObj, i ) + { + if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) ) + continue; + if ( Aig_ObjIsPi(pObj) ) + { + // copy the PI + pObjNew = Aig_ObjCreatePi(pNew); + pObj->pData = pObjNew; + pObjNew->pHaig = pObj->pHaig; + // set the arrival time of the new PI + arrTime = Tim_ManGetCiArrival( (Tim_Man_t *)p->pManTime, Aig_ObjPioNum(pObj) ); + pObjNew->Level = (int)arrTime; + } + else if ( Aig_ObjIsPo(pObj) ) + { + // perform balancing + pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); + pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel ); + 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_ObjPioNum(pObj), arrTime ); + // create PO + pObjNew = Aig_ObjCreatePo( pNew, pObjNew ); + pObjNew->pHaig = pObj->pHaig; + } + else + assert( 0 ); + } + Aig_ManCleanPioNumbers( p ); + pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 ); + } + else + { + Aig_ManForEachPi( p, pObj, i ) + { + pObjNew = Aig_ObjCreatePi(pNew); + pObjNew->Level = pObj->Level; + pObj->pData = pObjNew; + pObjNew->pHaig = pObj->pHaig; + } + Aig_ManForEachPo( p, pObj, i ) + { + pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); + pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel ); + pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) ); + pObjNew = Aig_ObjCreatePo( pNew, pObjNew ); + pObjNew->pHaig = pObj->pHaig; + } + } + 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 + |