diff options
Diffstat (limited to 'src/abc8/aig/aigDfs.c')
| -rw-r--r-- | src/abc8/aig/aigDfs.c | 723 |
1 files changed, 723 insertions, 0 deletions
diff --git a/src/abc8/aig/aigDfs.c b/src/abc8/aig/aigDfs.c new file mode 100644 index 00000000..c7488487 --- /dev/null +++ b/src/abc8/aig/aigDfs.c @@ -0,0 +1,723 @@ +/**CFile**************************************************************** + + FileName [aigDfs.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [DFS traversal procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigDfs.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManDfs_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + if ( pObj == NULL ) + return; + assert( !Aig_IsComplement(pObj) ); + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; +// assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) ); + Aig_ManDfs_rec( p, Aig_ObjFanin0(pObj), vNodes ); + Aig_ManDfs_rec( p, Aig_ObjFanin1(pObj), vNodes ); + assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection + Aig_ObjSetTravIdCurrent(p, pObj); + Vec_PtrPush( vNodes, pObj ); +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p ) +{ + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i; + Aig_ManIncrementTravId( p ); + // mark constant and PIs + Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) ); + Aig_ManForEachPi( p, pObj, i ) + Aig_ObjSetTravIdCurrent( p, pObj ); + // if there are latches, mark them + if ( Aig_ManLatchNum(p) > 0 ) + Aig_ManForEachObj( p, pObj, i ) + if ( Aig_ObjIsLatch(pObj) ) + Aig_ObjSetTravIdCurrent( p, pObj ); + // go through the nodes + vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) ); + Aig_ManForEachObj( p, pObj, i ) + if ( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) ) + Aig_ManDfs_rec( p, pObj, vNodes ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManDfsPio( Aig_Man_t * p ) +{ + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i; + Aig_ManIncrementTravId( p ); + vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) ); + Aig_ManForEachPo( p, pObj, i ) + Aig_ManDfs_rec( p, pObj, vNodes ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes ) +{ + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i; + assert( Aig_ManLatchNum(p) == 0 ); + Aig_ManIncrementTravId( p ); + // mark constant and PIs + Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) ); + Aig_ManForEachPi( p, pObj, i ) + Aig_ObjSetTravIdCurrent( p, pObj ); + // go through the nodes + vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) ); + for ( i = 0; i < nNodes; i++ ) + Aig_ManDfs_rec( p, ppNodes[i], vNodes ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManDfsChoices_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + if ( pObj == NULL ) + return; + assert( !Aig_IsComplement(pObj) ); + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + assert( Aig_ObjIsNode(pObj) ); + Aig_ManDfsChoices_rec( p, Aig_ObjFanin0(pObj), vNodes ); + Aig_ManDfsChoices_rec( p, Aig_ObjFanin1(pObj), vNodes ); + Aig_ManDfsChoices_rec( p, p->pEquivs[pObj->Id], vNodes ); + assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection + Aig_ObjSetTravIdCurrent(p, pObj); + Vec_PtrPush( vNodes, pObj ); +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p ) +{ + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i; + assert( p->pEquivs != NULL ); + Aig_ManIncrementTravId( p ); + // mark constant and PIs + Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) ); + Aig_ManForEachPi( p, pObj, i ) + Aig_ObjSetTravIdCurrent( p, pObj ); + // go through the nodes + vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) ); + Aig_ManForEachPo( p, pObj, i ) + Aig_ManDfsChoices_rec( p, Aig_ObjFanin0(pObj), vNodes ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the reverse DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManDfsReverse_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + Aig_Obj_t * pFanout; + int iFanout = -1, i; + assert( !Aig_IsComplement(pObj) ); + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) ); + Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i ) + Aig_ManDfsReverse_rec( p, pFanout, vNodes ); + assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection + Aig_ObjSetTravIdCurrent(p, pObj); + Vec_PtrPush( vNodes, pObj ); +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the reverse DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p ) +{ + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i; + Aig_ManIncrementTravId( p ); + // mark POs + Aig_ManForEachPo( p, pObj, i ) + Aig_ObjSetTravIdCurrent( p, pObj ); + // if there are latches, mark them + if ( Aig_ManLatchNum(p) > 0 ) + Aig_ManForEachObj( p, pObj, i ) + if ( Aig_ObjIsLatch(pObj) ) + Aig_ObjSetTravIdCurrent( p, pObj ); + // go through the nodes + vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) ); + Aig_ManForEachObj( p, pObj, i ) + if ( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) ) + Aig_ManDfsReverse_rec( p, pObj, vNodes ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Computes the max number of levels in the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManLevelNum( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i, LevelsMax; + LevelsMax = 0; + Aig_ManForEachPo( p, pObj, i ) + LevelsMax = AIG_MAX( LevelsMax, (int)Aig_ObjFanin0(pObj)->Level ); + return LevelsMax; +} + +/**Function************************************************************* + + Synopsis [Computes the max number of levels in the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManCountLevels( Aig_Man_t * p ) +{ + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i, LevelsMax, Level0, Level1; + // initialize the levels + Aig_ManConst1(p)->iData = 0; + Aig_ManForEachPi( p, pObj, i ) + pObj->iData = 0; + // compute levels in a DFS order + vNodes = Aig_ManDfs( p ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + Level0 = Aig_ObjFanin0(pObj)->iData; + Level1 = Aig_ObjFanin1(pObj)->iData; + pObj->iData = 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Level0, Level1); + } + Vec_PtrFree( vNodes ); + // get levels of the POs + LevelsMax = 0; + Aig_ManForEachPo( p, pObj, i ) + LevelsMax = AIG_MAX( LevelsMax, Aig_ObjFanin0(pObj)->iData ); + return LevelsMax; +} + +/**Function************************************************************* + + Synopsis [Counts the number of AIG nodes rooted at this cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ConeMark_rec( Aig_Obj_t * pObj ) +{ + assert( !Aig_IsComplement(pObj) ); + if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) ) + return; + Aig_ConeMark_rec( Aig_ObjFanin0(pObj) ); + Aig_ConeMark_rec( Aig_ObjFanin1(pObj) ); + assert( !Aig_ObjIsMarkA(pObj) ); // loop detection + Aig_ObjSetMarkA( pObj ); +} + +/**Function************************************************************* + + Synopsis [Counts the number of AIG nodes rooted at this cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ConeCleanAndMark_rec( Aig_Obj_t * pObj ) +{ + assert( !Aig_IsComplement(pObj) ); + if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) ) + return; + Aig_ConeCleanAndMark_rec( Aig_ObjFanin0(pObj) ); + Aig_ConeCleanAndMark_rec( Aig_ObjFanin1(pObj) ); + assert( !Aig_ObjIsMarkA(pObj) ); // loop detection + Aig_ObjSetMarkA( pObj ); + pObj->pData = NULL; +} + +/**Function************************************************************* + + Synopsis [Counts the number of AIG nodes rooted at this cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ConeCountAndMark_rec( Aig_Obj_t * pObj ) +{ + int Counter; + assert( !Aig_IsComplement(pObj) ); + if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) ) + return 0; + Counter = 1 + Aig_ConeCountAndMark_rec( Aig_ObjFanin0(pObj) ) + + Aig_ConeCountAndMark_rec( Aig_ObjFanin1(pObj) ); + assert( !Aig_ObjIsMarkA(pObj) ); // loop detection + Aig_ObjSetMarkA( pObj ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the number of AIG nodes rooted at this cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ConeUnmark_rec( Aig_Obj_t * pObj ) +{ + assert( !Aig_IsComplement(pObj) ); + if ( !Aig_ObjIsNode(pObj) || !Aig_ObjIsMarkA(pObj) ) + return; + Aig_ConeUnmark_rec( Aig_ObjFanin0(pObj) ); + Aig_ConeUnmark_rec( Aig_ObjFanin1(pObj) ); + assert( Aig_ObjIsMarkA(pObj) ); // loop detection + Aig_ObjClearMarkA( pObj ); +} + +/**Function************************************************************* + + Synopsis [Counts the number of AIG nodes rooted at this cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_DagSize( Aig_Obj_t * pObj ) +{ + int Counter; + Counter = Aig_ConeCountAndMark_rec( Aig_Regular(pObj) ); + Aig_ConeUnmark_rec( Aig_Regular(pObj) ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the support size of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_SupportSize_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int * pCounter ) +{ + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p, pObj); + if ( Aig_ObjIsPi(pObj) ) + { + (*pCounter)++; + return; + } + assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) ); + Aig_SupportSize_rec( p, Aig_ObjFanin0(pObj), pCounter ); + if ( Aig_ObjFanin1(pObj) ) + Aig_SupportSize_rec( p, Aig_ObjFanin1(pObj), pCounter ); +} + +/**Function************************************************************* + + Synopsis [Counts the support size of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + int Counter = 0; + assert( !Aig_IsComplement(pObj) ); + assert( !Aig_ObjIsPo(pObj) ); + Aig_ManIncrementTravId( p ); + Aig_SupportSize_rec( p, pObj, &Counter ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Transfers the AIG from one manager into another.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_Transfer_rec( Aig_Man_t * pDest, Aig_Obj_t * pObj ) +{ + assert( !Aig_IsComplement(pObj) ); + if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) ) + return; + Aig_Transfer_rec( pDest, Aig_ObjFanin0(pObj) ); + Aig_Transfer_rec( pDest, Aig_ObjFanin1(pObj) ); + pObj->pData = Aig_And( pDest, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + assert( !Aig_ObjIsMarkA(pObj) ); // loop detection + Aig_ObjSetMarkA( pObj ); +} + +/**Function************************************************************* + + Synopsis [Transfers the AIG from one manager into another.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pRoot, int nVars ) +{ + Aig_Obj_t * pObj; + int i; + // solve simple cases + if ( pSour == pDest ) + return pRoot; + if ( Aig_ObjIsConst1( Aig_Regular(pRoot) ) ) + return Aig_NotCond( Aig_ManConst1(pDest), Aig_IsComplement(pRoot) ); + // set the PI mapping + Aig_ManForEachPi( pSour, pObj, i ) + { + if ( i == nVars ) + break; + pObj->pData = Aig_IthVar(pDest, i); + } + // transfer and set markings + Aig_Transfer_rec( pDest, Aig_Regular(pRoot) ); + // clear the markings + Aig_ConeUnmark_rec( Aig_Regular(pRoot) ); + return Aig_NotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) ); +} + +/**Function************************************************************* + + Synopsis [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_Compose_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFunc, Aig_Obj_t * pVar ) +{ + assert( !Aig_IsComplement(pObj) ); + if ( Aig_ObjIsMarkA(pObj) ) + return; + if ( Aig_ObjIsConst1(pObj) || Aig_ObjIsPi(pObj) ) + { + pObj->pData = pObj == pVar ? pFunc : pObj; + return; + } + Aig_Compose_rec( p, Aig_ObjFanin0(pObj), pFunc, pVar ); + Aig_Compose_rec( p, Aig_ObjFanin1(pObj), pFunc, pVar ); + pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + assert( !Aig_ObjIsMarkA(pObj) ); // loop detection + Aig_ObjSetMarkA( pObj ); +} + +/**Function************************************************************* + + Synopsis [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar ) +{ + // quit if the PI variable is not defined + if ( iVar >= Aig_ManPiNum(p) ) + { + printf( "Aig_Compose(): The PI variable %d is not defined.\n", iVar ); + return NULL; + } + // recursively perform composition + Aig_Compose_rec( p, Aig_Regular(pRoot), pFunc, Aig_ManPi(p, iVar) ); + // clear the markings + Aig_ConeUnmark_rec( Aig_Regular(pRoot) ); + return Aig_NotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) ); +} + +/**Function************************************************************* + + Synopsis [Computes the internal nodes of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ObjCollectCut_rec( Aig_Obj_t * pNode, Vec_Ptr_t * vNodes ) +{ +// Aig_Obj_t * pFan0 = Aig_ObjFanin0(pNode); +// Aig_Obj_t * pFan1 = Aig_ObjFanin1(pNode); + if ( pNode->fMarkA ) + return; + pNode->fMarkA = 1; + assert( Aig_ObjIsNode(pNode) ); + Aig_ObjCollectCut_rec( Aig_ObjFanin0(pNode), vNodes ); + Aig_ObjCollectCut_rec( Aig_ObjFanin1(pNode), vNodes ); + Vec_PtrPush( vNodes, pNode ); +//printf( "added %d ", pNode->Id ); +} + +/**Function************************************************************* + + Synopsis [Computes the internal nodes of the cut.] + + Description [Does not include the leaves of the cut.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes ) +{ + Aig_Obj_t * pObj; + int i; + // collect and mark the leaves + Vec_PtrClear( vNodes ); + Vec_PtrForEachEntry( vLeaves, pObj, i ) + { + assert( pObj->fMarkA == 0 ); + pObj->fMarkA = 1; +// printf( "%d " , pObj->Id ); + } +//printf( "\n" ); + // collect and mark the nodes + Aig_ObjCollectCut_rec( pRoot, vNodes ); + // clean the nodes + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->fMarkA = 0; + Vec_PtrForEachEntry( vLeaves, pObj, i ) + pObj->fMarkA = 0; +} + + +/**Function************************************************************* + + Synopsis [Collects the nodes of the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ObjCollectSuper_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)->fMarkA ) + { + // 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_PtrPush( vSuper, pObj ); + Aig_Regular(pObj)->fMarkA = 1; + return 0; + } + assert( !Aig_IsComplement(pObj) ); + assert( Aig_ObjIsNode(pObj) ); + // go through the branches + RetValue1 = Aig_ObjCollectSuper_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper ); + RetValue2 = Aig_ObjCollectSuper_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 [] + +***********************************************************************/ +int Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper ) +{ + int RetValue, i; + assert( !Aig_IsComplement(pObj) ); + assert( Aig_ObjIsNode(pObj) ); + // collect the nodes in the implication supergate + Vec_PtrClear( vSuper ); + RetValue = Aig_ObjCollectSuper_rec( pObj, pObj, vSuper ); + assert( Vec_PtrSize(vSuper) > 1 ); + // unmark the visited nodes + Vec_PtrForEachEntry( vSuper, pObj, i ) + Aig_Regular(pObj)->fMarkA = 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 ) + vSuper->nSize = 0; + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |