From c2ab4426e425375645cb253dacef67946aaad3c7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 26 Mar 2012 15:01:54 -0700 Subject: Important bug fix in XOR balancing (balance -x). --- src/opt/dar/darBalance.c | 276 ++++++++++++++++------------------------------- 1 file changed, 91 insertions(+), 185 deletions(-) (limited to 'src/opt/dar') diff --git a/src/opt/dar/darBalance.c b/src/opt/dar/darBalance.c index 484b86e7..34559bec 100644 --- a/src/opt/dar/darBalance.c +++ b/src/opt/dar/darBalance.c @@ -34,15 +34,9 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// - - -static inline word Dar_BalPack( int Lev, int Id ) { return (((word)Lev) << 32) | Id; } -static inline int Dar_BalUnpackLev( word Num ) { return (Num >> 32); } -static inline int Dar_BalUnpackId( word Num ) { return Num & 0xFFFF; } - /**Function************************************************************* - Synopsis [Collects one multi-input gate.] + Synopsis [Uniqifies the node.] Description [] @@ -51,131 +45,92 @@ static inline int Dar_BalUnpackId( word Num ) { return Num & 0xFFFF; SeeAlso [] ***********************************************************************/ -Vec_Wrd_t * Dar_BalSuperXor( Aig_Man_t * p, Aig_Obj_t * pObj, int * pfCompl ) +int Dar_ObjCompareLits( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 ) { - Aig_Obj_t * pObj0, * pObj1, * pRoot = NULL; - Vec_Wrd_t * vSuper; - word Num, NumNext; - int i, k, fCompl = 0; - assert( !Aig_IsComplement(pObj) ); - assert( Aig_ObjIsExor(pObj) ); - // start iteration - vSuper = Vec_WrdAlloc( 10 ); - Vec_WrdPush( vSuper, Dar_BalPack(Aig_ObjLevel(pObj), Aig_ObjId(pObj)) ); - while ( Vec_WrdSize(vSuper) > 0 && Vec_WrdSize(vSuper) < 10000 ) - { - // make sure there are no duplicates - Num = Vec_WrdEntry( vSuper, 0 ); - Vec_WrdForEachEntryStart( vSuper, NumNext, i, 1 ) - { - assert( Num < NumNext ); - Num = NumNext; - } - // extract XOR gate decomposable on the topmost level - Vec_WrdForEachEntryReverse( vSuper, Num, i ) - { - pRoot = Aig_ManObj( p, Dar_BalUnpackId(Num) ); - if ( Aig_ObjIsExor(pRoot) && Aig_ObjRefs(pRoot) == 1 ) - { - Vec_WrdRemove( vSuper, Num ); - break; - } - } - if ( i == -1 ) - break; - // extract - assert( !Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) ); - pObj0 = Aig_ObjChild0(pObj); - pObj1 = Aig_ObjChild1(pObj); - fCompl ^= Aig_IsComplement(pObj0); pObj0 = Aig_Regular(pObj0); - fCompl ^= Aig_IsComplement(pObj1); pObj1 = Aig_Regular(pObj1); - Vec_WrdPushOrder( vSuper, Dar_BalPack(Aig_ObjLevel(pObj0), Aig_ObjId(pObj0)) ); - Vec_WrdPushOrder( vSuper, Dar_BalPack(Aig_ObjLevel(pObj1), Aig_ObjId(pObj1)) ); - // remove duplicates - k = 0; - Vec_WrdForEachEntry( vSuper, Num, i ) - { - if ( i + 1 == Vec_WrdSize(vSuper) ) - { - Vec_WrdWriteEntry( vSuper, k++, Num ); - break; - } - NumNext = Vec_WrdEntry( vSuper, i+1 ); - assert( Num <= NumNext ); - if ( Num == NumNext ) - i++; - else - Vec_WrdWriteEntry( vSuper, k++, Num ); - } - Vec_WrdShrink( vSuper, k ); - } - *pfCompl = fCompl; - Vec_WrdForEachEntry( vSuper, Num, i ) - Vec_WrdWriteEntry( vSuper, i, Dar_BalUnpackId(Num) ); - return vSuper; + int Diff = Aig_ObjToLit(*pp1) - Aig_ObjToLit(*pp2); + if ( Diff < 0 ) + return -1; + if ( Diff > 0 ) + return 1; + return 0; } -Vec_Wrd_t * Dar_BalSuperAnd( Aig_Man_t * p, Aig_Obj_t * pObj ) +void Dar_BalanceUniqify( Aig_Obj_t * pObj, Vec_Ptr_t * vNodes, int fExor ) { - Aig_Obj_t * pObj0, * pObj1, * pRoot = NULL; - Vec_Wrd_t * vSuper; - word Num, NumNext; + Aig_Obj_t * pTemp, * pTempNext; int i, k; - assert( !Aig_IsComplement(pObj) ); - // start iteration - vSuper = Vec_WrdAlloc( 10 ); - Vec_WrdPush( vSuper, Dar_BalPack(Aig_ObjLevel(pObj), Aig_ObjToLit(pObj)) ); - while ( Vec_WrdSize(vSuper) > 0 && Vec_WrdSize(vSuper) < 10000 ) + // sort the nodes by their literal + Vec_PtrSort( vNodes, (int (*)())Dar_ObjCompareLits ); + // remove duplicates + k = 0; + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pTemp, i ) { - // make sure there are no duplicates - Num = Vec_WrdEntry( vSuper, 0 ); - Vec_WrdForEachEntryStart( vSuper, NumNext, i, 1 ) - { - assert( Num < NumNext ); - Num = NumNext; - } - // extract AND gate decomposable on the topmost level - Vec_WrdForEachEntryReverse( vSuper, Num, i ) + if ( i + 1 == Vec_PtrSize(vNodes) ) { - pRoot = Aig_ObjFromLit( p, Dar_BalUnpackId(Num) ); - if ( !Aig_IsComplement(pRoot) && Aig_ObjIsNode(pRoot) && Aig_ObjRefs(pRoot) == 1 ) - { - Vec_WrdRemove( vSuper, Num ); - break; - } - } - if ( i == -1 ) + Vec_PtrWriteEntry( vNodes, k++, pTemp ); break; - // extract - pObj0 = Aig_ObjChild0(pRoot); - pObj1 = Aig_ObjChild1(pRoot); - Vec_WrdPushOrder( vSuper, Dar_BalPack(Aig_ObjLevel(Aig_Regular(pObj0)), Aig_ObjToLit(pObj0)) ); - Vec_WrdPushOrder( vSuper, Dar_BalPack(Aig_ObjLevel(Aig_Regular(pObj1)), Aig_ObjToLit(pObj1)) ); - // remove duplicates - k = 0; - Vec_WrdForEachEntry( vSuper, Num, i ) + } + pTempNext = (Aig_Obj_t *)Vec_PtrEntry( vNodes, i+1 ); + if ( !fExor && pTemp == Aig_Not(pTempNext) ) // pos_lit & neg_lit = 0 { - if ( i + 1 == Vec_WrdSize(vSuper) ) - { - Vec_WrdWriteEntry( vSuper, k++, Num ); - break; - } - NumNext = Vec_WrdEntry( vSuper, i+1 ); - assert( Num <= NumNext ); - if ( Num + 1 == NumNext && (NumNext & 1) ) // pos_lit & neg_lit = 0 - { - Vec_WrdClear( vSuper ); - return vSuper; - } - if ( Num < NumNext ) - Vec_WrdWriteEntry( vSuper, k++, Num ); + Vec_PtrClear( vNodes ); + return; } - Vec_WrdShrink( vSuper, k ); + 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 ); + // 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; } - Vec_WrdForEachEntry( vSuper, Num, i ) - Vec_WrdWriteEntry( vSuper, i, Dar_BalUnpackId(Num) ); - return vSuper; } +/**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************************************************************* @@ -189,6 +144,7 @@ Vec_Wrd_t * Dar_BalSuperAnd( Aig_Man_t * p, Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ +/* int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper ) { int RetValue1, RetValue2, i; @@ -235,19 +191,7 @@ int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper // 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_Man_t * p, Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level ) +Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level ) { Vec_Ptr_t * vNodes; int RetValue, i; @@ -270,50 +214,7 @@ Vec_Ptr_t * Dar_BalanceCone( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Vec_t * vStore vNodes->nSize = 0; return vNodes; } - -/**Function************************************************************* - - Synopsis [Collects the nodes of the supergate.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Dar_BalanceCone_( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level ) -{ - Vec_Wrd_t * vSuper; - Vec_Ptr_t * vNodes; - word Num; - int 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 - // load the result into the output array - if ( Aig_ObjIsExor(pObj) ) - { - int fCompl = 0; - vSuper = Dar_BalSuperXor( p, pObj, &fCompl ); - Vec_WrdForEachEntry( vSuper, Num, i ) - Vec_PtrPush( vNodes, Aig_ManObj(p, Dar_BalUnpackId(Num)) ); - assert( fCompl == 0 ); - } - else - { - vSuper = Dar_BalSuperAnd( p, pObj ); - Vec_WrdForEachEntry( vSuper, Num, i ) - Vec_PtrPush( vNodes, Aig_ObjFromLit(p, Dar_BalUnpackId(Num)) ); - } - Vec_WrdFree( vSuper ); - return vNodes; -} +*/ /**Function************************************************************* @@ -460,12 +361,16 @@ int Aig_NodeCompareLevelsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 ) SeeAlso [] ***********************************************************************/ -void Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj ) +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-- ) { @@ -506,7 +411,7 @@ Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t // 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) ); + Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type), Type == AIG_OBJ_EXOR ); } return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0); } @@ -576,7 +481,7 @@ Aig_Obj_t * Dar_BalanceBuildSuperTop( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Typ pObj = Dar_BalanceBuildSuper( p, vSubset, Type, fUpdateLevel ); Vec_PtrFree( vSubset ); // add the new output - Dar_BalancePushUniqueOrderByLevel( vSuper, pObj ); + Dar_BalancePushUniqueOrderByLevel( vSuper, pObj, Type == AIG_OBJ_EXOR ); } return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0); } @@ -592,7 +497,7 @@ Aig_Obj_t * Dar_BalanceBuildSuperTop( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Typ SeeAlso [] ***********************************************************************/ -Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel ) +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; @@ -604,7 +509,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObjOl return (Aig_Obj_t *)pObjOld->pData; assert( Aig_ObjIsNode(pObjOld) ); // get the implication supergate - vSuper = Dar_BalanceCone( p, pObjOld, vStore, Level ); + 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)); @@ -615,7 +520,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObjOl // for each old node, derive the new well-balanced node for ( i = 0; i < Vec_PtrSize(vSuper); i++ ) { - pObjNew = Dar_Balance_rec( pNew, p, Aig_Regular((Aig_Obj_t *)vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel ); + 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 @@ -702,7 +607,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) { // perform balancing pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); - pObjNew = Dar_Balance_rec( pNew, p, Aig_Regular(pDriver), vStore, 0, fUpdateLevel ); + 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; @@ -729,7 +634,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) Aig_ManForEachCo( p, pObj, i ) { pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); - pObjNew = Dar_Balance_rec( pNew, p, Aig_Regular(pDriver), vStore, 0, fUpdateLevel ); + pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel ); pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) ); pObjNew = Aig_ObjCreateCo( pNew, pObjNew ); pObjNew->pHaig = pObj->pHaig; @@ -828,5 +733,6 @@ void Dar_BalancePrintStats( Aig_Man_t * p ) /// END OF FILE /// //////////////////////////////////////////////////////////////////////// + ABC_NAMESPACE_IMPL_END -- cgit v1.2.3