diff options
Diffstat (limited to 'src/aig/dar')
| -rw-r--r-- | src/aig/dar/darBalance.c | 456 | ||||
| -rw-r--r-- | src/aig/dar/darScript.c | 8 |
2 files changed, 255 insertions, 209 deletions
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c index 03707481..63f6f232 100644 --- a/src/aig/dar/darBalance.c +++ b/src/aig/dar/darBalance.c @@ -25,151 +25,12 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level, int fUpdateLevel ); -static Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level ); -static int Dar_BalanceFindLeft( Vec_Ptr_t * vSuper ); -static void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor ); -static void Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj ); -static Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**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; - // create the new manager - pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); - pNew->nRegs = p->nRegs; - pNew->nAsserts = p->nAsserts; - 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( p->pManTime ); - Aig_ManSetPioNumbers( p ); - Aig_ManForEachObj( p, pObj, i ) - { - if ( Aig_ObjIsAnd(pObj) || Aig_ObjIsConst1(pObj) ) - continue; - if ( Aig_ObjIsPi(pObj) ) - { - // copy the PI - pObjNew = Aig_ObjCreatePi(pNew); - pObj->pData = pObjNew; - // set the arrival time of the new PI - arrTime = Tim_ManGetPiArrival( 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) ); - Aig_ObjCreatePo( pNew, pObjNew ); - // save arrival time of the output - arrTime = (float)Aig_Regular(pObjNew)->Level; - Tim_ManSetPoArrival( p->pManTime, Aig_ObjPioNum(pObj), arrTime ); - } - else - assert( 0 ); - } - Aig_ManCleanPioNumbers( p ); - pNew->pManTime = Tim_ManDup( p->pManTime, 0 ); - } - else - { - Aig_ManForEachPi( p, pObj, i ) - { - pObjNew = Aig_ObjCreatePi(pNew); - pObjNew->Level = pObj->Level; - pObj->pData = pObjNew; - } - 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) ); - Aig_ObjCreatePo( pNew, pObjNew ); - } - } - Vec_VecFree( vStore ); - // remove dangling nodes - Aig_ManCleanup( pNew ); - // check the resulting AIG - if ( !Aig_ManCheck(pNew) ) - printf( "Dar_ManBalance(): The check has failed.\n" ); - return pNew; -} - -/**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 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 pObjOld->pData = Aig_ManConst0(pNew); - if ( Vec_PtrSize(vSuper) < 2 ) - printf( "BUG!\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(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel ); - vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement(vSuper->pArray[i]) ); - } - // build the supergate - pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel ); - // make sure the balanced node is not assigned -// assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level ); - assert( pObjOld->pData == NULL ); - Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig; - return pObjOld->pData = pObjNew; -} - -/**Function************************************************************* - Synopsis [Collects the nodes of the supergate.] Description [] @@ -185,14 +46,26 @@ int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper // check if the node is visited if ( Aig_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] == Aig_Not(pObj) ) - return -1; + 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; } @@ -251,60 +124,6 @@ Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level ) /**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; - return 0; -} - -/**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, 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 = Vec_PtrPop(vSuper); - pObj2 = Vec_PtrPop(vSuper); - Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type) ); - } - return Vec_PtrEntry(vSuper, 0); -} - -/**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. @@ -405,6 +224,27 @@ void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int f /**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; + return 0; +} + +/**Function************************************************************* + Synopsis [Inserts a new node in the order by levels.] Description [] @@ -432,6 +272,220 @@ void Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj ) } } +/**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, 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 = Vec_PtrPop(vSuper); + pObj2 = Vec_PtrPop(vSuper); + Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type) ); + } + return 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 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 pObjOld->pData = Aig_ManConst0(pNew); + if ( Vec_PtrSize(vSuper) < 2 ) + printf( "BUG!\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(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel ); + vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement(vSuper->pArray[i]) ); + } + // build the supergate + pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel ); + // make sure the balanced node is not assigned +// assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level ); + assert( pObjOld->pData == NULL ); + Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig; + return 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; + // create the new manager + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->nRegs = p->nRegs; + pNew->nAsserts = p->nAsserts; + 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( 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; + // set the arrival time of the new PI + arrTime = Tim_ManGetPiArrival( 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) ); + Aig_ObjCreatePo( pNew, pObjNew ); + // save arrival time of the output + arrTime = (float)Aig_Regular(pObjNew)->Level; + Tim_ManSetPoArrival( p->pManTime, Aig_ObjPioNum(pObj), arrTime ); + } + else + assert( 0 ); + } + Aig_ManCleanPioNumbers( p ); + pNew->pManTime = Tim_ManDup( p->pManTime, 0 ); + } + else + { + Aig_ManForEachPi( p, pObj, i ) + { + pObjNew = Aig_ObjCreatePi(pNew); + pObjNew->Level = pObj->Level; + pObj->pData = pObjNew; + } + 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) ); + Aig_ObjCreatePo( pNew, pObjNew ); + } + } + Vec_VecFree( vStore ); + // remove dangling nodes + Aig_ManCleanup( pNew ); + // check the resulting AIG + if ( !Aig_ManCheck(pNew) ) + printf( "Dar_ManBalance(): The check has failed.\n" ); + return pNew; +} + +/**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( vSuper, pTemp, k ) + pTemp->fMarkB = 0; + if ( Vec_PtrSize(vSuper) < 3 ) + continue; + printf( " %d(", Vec_PtrSize(vSuper) ); + Vec_PtrForEachEntry( vSuper, pTemp, k ) + printf( " %d", pTemp->Level ); + printf( " )" ); + } + Vec_PtrFree( vSuper ); + Aig_ManForEachObj( p, pObj, i ) + pObj->fMarkA = 0; + printf( "\n" ); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c index a4ac9082..116b1591 100644 --- a/src/aig/dar/darScript.c +++ b/src/aig/dar/darScript.c @@ -201,14 +201,6 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i Aig_ManStop( pTemp ); if ( fVerbose ) Aig_ManPrintStats( pAig ); - // balance - if ( fBalance ) - { - pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); - Aig_ManStop( pTemp ); - if ( fVerbose ) Aig_ManPrintStats( pAig ); - } - return pAig; } |