| /**CFile**************************************************************** |
| |
| FileName [saigWnd.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Sequential AIG package.] |
| |
| Synopsis [Sequential windowing.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: saigWnd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "saig.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the array of PI/internal nodes.] |
| |
| Description [Marks all the visited nodes with the current ID. |
| Does not collect constant node and PO/LI nodes.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Saig_ManWindowOutline_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist, Vec_Ptr_t * vNodes, int * pDists ) |
| { |
| Aig_Obj_t * pMatch, * pFanout; |
| int fCollected, iFanout = -1, i; |
| if ( nDist == 0 ) |
| return; |
| if ( pDists[pObj->Id] >= nDist ) |
| return; |
| pDists[pObj->Id] = nDist; |
| fCollected = Aig_ObjIsTravIdCurrent( p, pObj ); |
| Aig_ObjSetTravIdCurrent( p, pObj ); |
| if ( Aig_ObjIsConst1(pObj) ) |
| return; |
| if ( Saig_ObjIsPo(p, pObj) ) |
| return; |
| if ( Saig_ObjIsLi(p, pObj) ) |
| { |
| pMatch = Saig_ObjLiToLo( p, pObj ); |
| if ( !Aig_ObjIsTravIdCurrent( p, pMatch ) ) |
| Saig_ManWindowOutline_rec( p, pMatch, nDist, vNodes, pDists ); |
| Saig_ManWindowOutline_rec( p, Aig_ObjFanin0(pObj), nDist-1, vNodes, pDists ); |
| return; |
| } |
| if ( !fCollected ) |
| Vec_PtrPush( vNodes, pObj ); |
| if ( Saig_ObjIsPi(p, pObj) ) |
| return; |
| if ( Saig_ObjIsLo(p, pObj) ) |
| { |
| pMatch = Saig_ObjLoToLi( p, pObj ); |
| if ( !Aig_ObjIsTravIdCurrent( p, pMatch ) ) |
| Saig_ManWindowOutline_rec( p, pMatch, nDist, vNodes, pDists ); |
| Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i ) |
| Saig_ManWindowOutline_rec( p, pFanout, nDist-1, vNodes, pDists ); |
| return; |
| } |
| assert( Aig_ObjIsNode(pObj) ); |
| Saig_ManWindowOutline_rec( p, Aig_ObjFanin0(pObj), nDist-1, vNodes, pDists ); |
| Saig_ManWindowOutline_rec( p, Aig_ObjFanin1(pObj), nDist-1, vNodes, pDists ); |
| Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i ) |
| Saig_ManWindowOutline_rec( p, pFanout, nDist-1, vNodes, pDists ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the array of PI/internal nodes.] |
| |
| Description [Marks all the visited nodes with the current ID.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Ptr_t * Saig_ManWindowOutline( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist ) |
| { |
| Vec_Ptr_t * vNodes; |
| Aig_Obj_t * pObjLi, * pObjLo; |
| int * pDists, i; |
| pDists = ABC_CALLOC( int, Aig_ManObjNumMax(p) ); |
| vNodes = Vec_PtrAlloc( 1000 ); |
| Aig_ManIncrementTravId( p ); |
| Saig_ManWindowOutline_rec( p, pObj, nDist, vNodes, pDists ); |
| Vec_PtrSort( vNodes, (int (*)(void))Aig_ObjCompareIdIncrease ); |
| // make sure LI/LO are labeled/unlabeled mutually |
| Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) |
| assert( Aig_ObjIsTravIdCurrent(p, pObjLi) == |
| Aig_ObjIsTravIdCurrent(p, pObjLo) ); |
| ABC_FREE( pDists ); |
| return vNodes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if the node has unlabeled fanout.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Obj_t * Saig_ObjHasUnlabeledFanout( Aig_Man_t * p, Aig_Obj_t * pObj ) |
| { |
| Aig_Obj_t * pFanout; |
| int iFanout = -1, i; |
| Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i ) |
| if ( Saig_ObjIsPo(p, pFanout) || !Aig_ObjIsTravIdCurrent(p, pFanout) ) |
| return pFanout; |
| return NULL; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collects primary inputs.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Ptr_t * Saig_ManWindowCollectPis( Aig_Man_t * p, Vec_Ptr_t * vNodes ) |
| { |
| Vec_Ptr_t * vNodesPi; |
| Aig_Obj_t * pObj, * pMatch, * pFanin; |
| int i; |
| vNodesPi = Vec_PtrAlloc( 1000 ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) |
| { |
| if ( Saig_ObjIsPi(p, pObj) ) |
| { |
| assert( pObj->pData == NULL ); |
| Vec_PtrPush( vNodesPi, pObj ); |
| } |
| else if ( Saig_ObjIsLo(p, pObj) ) |
| { |
| pMatch = Saig_ObjLoToLi( p, pObj ); |
| pFanin = Aig_ObjFanin0(pMatch); |
| if ( !Aig_ObjIsTravIdCurrent(p, pFanin) && pFanin->pData == NULL ) |
| Vec_PtrPush( vNodesPi, pFanin ); |
| } |
| else |
| { |
| assert( Aig_ObjIsNode(pObj) ); |
| pFanin = Aig_ObjFanin0(pObj); |
| if ( !Aig_ObjIsTravIdCurrent(p, pFanin) && pFanin->pData == NULL ) |
| Vec_PtrPush( vNodesPi, pFanin ); |
| pFanin = Aig_ObjFanin1(pObj); |
| if ( !Aig_ObjIsTravIdCurrent(p, pFanin) && pFanin->pData == NULL ) |
| Vec_PtrPush( vNodesPi, pFanin ); |
| } |
| } |
| return vNodesPi; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collects primary outputs.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Ptr_t * Saig_ManWindowCollectPos( Aig_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t ** pvPointers ) |
| { |
| Vec_Ptr_t * vNodesPo; |
| Aig_Obj_t * pObj, * pPointer; |
| int i; |
| vNodesPo = Vec_PtrAlloc( 1000 ); |
| if ( pvPointers ) |
| *pvPointers = Vec_PtrAlloc( 1000 ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) |
| { |
| if ( (pPointer = Saig_ObjHasUnlabeledFanout(p, pObj)) ) |
| { |
| Vec_PtrPush( vNodesPo, pObj ); |
| if ( pvPointers ) |
| Vec_PtrPush( *pvPointers, pPointer ); |
| } |
| } |
| return vNodesPo; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Extracts the window AIG from the AIG manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManWindowExtractNodes( Aig_Man_t * p, Vec_Ptr_t * vNodes ) |
| { |
| Aig_Man_t * pNew; |
| Aig_Obj_t * pObj, * pMatch; |
| Vec_Ptr_t * vNodesPi, * vNodesPo; |
| int i, nRegCount; |
| Aig_ManCleanData( p ); |
| // create the new manager |
| pNew = Aig_ManStart( Vec_PtrSize(vNodes) ); |
| pNew->pName = Abc_UtilStrsav( "wnd" ); |
| pNew->pSpec = NULL; |
| // map constant nodes |
| pObj = Aig_ManConst1( p ); |
| pObj->pData = Aig_ManConst1( pNew ); |
| // create real PIs |
| vNodesPi = Saig_ManWindowCollectPis( p, vNodes ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPi, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi(pNew); |
| Vec_PtrFree( vNodesPi ); |
| // create register outputs |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) |
| { |
| if ( Saig_ObjIsLo(p, pObj) ) |
| pObj->pData = Aig_ObjCreateCi(pNew); |
| } |
| // create internal nodes |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) |
| { |
| if ( Aig_ObjIsNode(pObj) ) |
| pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| } |
| // create POs |
| vNodesPo = Saig_ManWindowCollectPos( p, vNodes, NULL ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPo, pObj, i ) |
| Aig_ObjCreateCo( pNew, (Aig_Obj_t *)pObj->pData ); |
| Vec_PtrFree( vNodesPo ); |
| // create register inputs |
| nRegCount = 0; |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) |
| { |
| if ( Saig_ObjIsLo(p, pObj) ) |
| { |
| pMatch = Saig_ObjLoToLi( p, pObj ); |
| Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch) ); |
| nRegCount++; |
| } |
| } |
| Aig_ManSetRegNum( pNew, nRegCount ); |
| Aig_ManCleanup( pNew ); |
| return pNew; |
| } |
| |
| static void Saig_ManWindowInsertSmall_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjSmall, |
| Vec_Ptr_t * vBigNode2SmallPo, Vec_Ptr_t * vSmallPi2BigNode ); |
| |
| /**Function************************************************************* |
| |
| Synopsis [Adds nodes for the big manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Saig_ManWindowInsertBig_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjBig, |
| Vec_Ptr_t * vBigNode2SmallPo, Vec_Ptr_t * vSmallPi2BigNode ) |
| { |
| Aig_Obj_t * pMatch; |
| if ( pObjBig->pData ) |
| return; |
| if ( (pMatch = (Aig_Obj_t *)Vec_PtrEntry( vBigNode2SmallPo, pObjBig->Id )) ) |
| { |
| Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin0(pMatch), vBigNode2SmallPo, vSmallPi2BigNode ); |
| pObjBig->pData = Aig_ObjChild0Copy(pMatch); |
| return; |
| } |
| assert( Aig_ObjIsNode(pObjBig) ); |
| Saig_ManWindowInsertBig_rec( pNew, Aig_ObjFanin0(pObjBig), vBigNode2SmallPo, vSmallPi2BigNode ); |
| Saig_ManWindowInsertBig_rec( pNew, Aig_ObjFanin1(pObjBig), vBigNode2SmallPo, vSmallPi2BigNode ); |
| pObjBig->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObjBig), Aig_ObjChild1Copy(pObjBig) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Adds nodes for the small manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Saig_ManWindowInsertSmall_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjSmall, |
| Vec_Ptr_t * vBigNode2SmallPo, Vec_Ptr_t * vSmallPi2BigNode ) |
| { |
| Aig_Obj_t * pMatch; |
| if ( pObjSmall->pData ) |
| return; |
| if ( (pMatch = (Aig_Obj_t *)Vec_PtrEntry( vSmallPi2BigNode, pObjSmall->Id )) ) |
| { |
| Saig_ManWindowInsertBig_rec( pNew, pMatch, vBigNode2SmallPo, vSmallPi2BigNode ); |
| pObjSmall->pData = pMatch->pData; |
| return; |
| } |
| assert( Aig_ObjIsNode(pObjSmall) ); |
| Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin0(pObjSmall), vBigNode2SmallPo, vSmallPi2BigNode ); |
| Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin1(pObjSmall), vBigNode2SmallPo, vSmallPi2BigNode ); |
| pObjSmall->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObjSmall), Aig_ObjChild1Copy(pObjSmall) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Extracts the network from the AIG manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManWindowInsertNodes( Aig_Man_t * p, Vec_Ptr_t * vNodes, Aig_Man_t * pWnd ) |
| { |
| Aig_Man_t * pNew; |
| Vec_Ptr_t * vBigNode2SmallPo, * vSmallPi2BigNode; |
| Vec_Ptr_t * vNodesPi, * vNodesPo; |
| Aig_Obj_t * pObj; |
| int i; |
| |
| // set mapping of small PIs into big nodes |
| vSmallPi2BigNode = Vec_PtrStart( Aig_ManObjNumMax(pWnd) ); |
| vNodesPi = Saig_ManWindowCollectPis( p, vNodes ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPi, pObj, i ) |
| Vec_PtrWriteEntry( vSmallPi2BigNode, Aig_ManCi(pWnd, i)->Id, pObj ); |
| assert( i == Saig_ManPiNum(pWnd) ); |
| Vec_PtrFree( vNodesPi ); |
| |
| // set mapping of big nodes into small POs |
| vBigNode2SmallPo = Vec_PtrStart( Aig_ManObjNumMax(p) ); |
| vNodesPo = Saig_ManWindowCollectPos( p, vNodes, NULL ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPo, pObj, i ) |
| Vec_PtrWriteEntry( vBigNode2SmallPo, pObj->Id, Aig_ManCo(pWnd, i) ); |
| assert( i == Saig_ManPoNum(pWnd) ); |
| Vec_PtrFree( vNodesPo ); |
| |
| // create the new manager |
| Aig_ManCleanData( p ); |
| Aig_ManCleanData( pWnd ); |
| pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| // map constant nodes |
| pObj = Aig_ManConst1( p ); |
| pObj->pData = Aig_ManConst1( pNew ); |
| pObj = Aig_ManConst1( pWnd ); |
| pObj->pData = Aig_ManConst1( pNew ); |
| |
| // create real PIs |
| Aig_ManForEachCi( p, pObj, i ) |
| if ( Saig_ObjIsPi(p, pObj) || !Aig_ObjIsTravIdCurrent(p, pObj) ) |
| pObj->pData = Aig_ObjCreateCi(pNew); |
| // create additional latch outputs |
| Saig_ManForEachLo( pWnd, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi(pNew); |
| |
| // create internal nodes starting from the big |
| Aig_ManForEachCo( p, pObj, i ) |
| if ( Saig_ObjIsPo(p, pObj) || !Aig_ObjIsTravIdCurrent(p, pObj) ) |
| { |
| Saig_ManWindowInsertBig_rec( pNew, Aig_ObjFanin0(pObj), vBigNode2SmallPo, vSmallPi2BigNode ); |
| pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); |
| } |
| // create internal nodes starting from the small |
| Saig_ManForEachLi( pWnd, pObj, i ) |
| { |
| Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin0(pObj), vBigNode2SmallPo, vSmallPi2BigNode ); |
| pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); |
| } |
| Vec_PtrFree( vBigNode2SmallPo ); |
| Vec_PtrFree( vSmallPi2BigNode ); |
| // set the new number of registers |
| assert( Aig_ManCiNum(pNew) - Aig_ManCiNum(p) == Aig_ManCoNum(pNew) - Aig_ManCoNum(p) ); |
| Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) + (Aig_ManCiNum(pNew) - Aig_ManCiNum(p)) ); |
| Aig_ManCleanup( pNew ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Find a good object.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Obj_t * Saig_ManFindPivot( Aig_Man_t * p ) |
| { |
| Aig_Obj_t * pObj; |
| int i, Counter; |
| if ( Aig_ManRegNum(p) > 0 ) |
| { |
| if ( Aig_ManRegNum(p) == 1 ) |
| return Saig_ManLo( p, 0 ); |
| Saig_ManForEachLo( p, pObj, i ) |
| { |
| if ( i == Aig_ManRegNum(p)/2 ) |
| return pObj; |
| } |
| } |
| else |
| { |
| Counter = 0; |
| assert( Aig_ManNodeNum(p) > 1 ); |
| Aig_ManForEachNode( p, pObj, i ) |
| { |
| if ( Counter++ == Aig_ManNodeNum(p)/2 ) |
| return pObj; |
| } |
| } |
| return NULL; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes sequential window of the node.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManWindowExtract( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist ) |
| { |
| Aig_Man_t * pWnd; |
| Vec_Ptr_t * vNodes; |
| Aig_ManFanoutStart( p ); |
| vNodes = Saig_ManWindowOutline( p, pObj, nDist ); |
| pWnd = Saig_ManWindowExtractNodes( p, vNodes ); |
| Vec_PtrFree( vNodes ); |
| Aig_ManFanoutStop( p ); |
| return pWnd; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes sequential window of the node.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManWindowInsert( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist, Aig_Man_t * pWnd ) |
| { |
| Aig_Man_t * pNew, * pWndTest; |
| Vec_Ptr_t * vNodes; |
| Aig_ManFanoutStart( p ); |
| |
| vNodes = Saig_ManWindowOutline( p, pObj, nDist ); |
| pWndTest = Saig_ManWindowExtractNodes( p, vNodes ); |
| if ( Saig_ManPiNum(pWndTest) != Saig_ManPiNum(pWnd) || |
| Saig_ManPoNum(pWndTest) != Saig_ManPoNum(pWnd) ) |
| { |
| printf( "The window cannot be reinserted because PI/PO counts do not match.\n" ); |
| Aig_ManStop( pWndTest ); |
| Vec_PtrFree( vNodes ); |
| Aig_ManFanoutStop( p ); |
| return NULL; |
| } |
| Aig_ManStop( pWndTest ); |
| Vec_PtrFree( vNodes ); |
| |
| // insert the nodes |
| Aig_ManCleanData( p ); |
| vNodes = Saig_ManWindowOutline( p, pObj, nDist ); |
| pNew = Saig_ManWindowInsertNodes( p, vNodes, pWnd ); |
| Vec_PtrFree( vNodes ); |
| Aig_ManFanoutStop( p ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Tests the above computation.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManWindowTest( Aig_Man_t * p ) |
| { |
| int nDist = 3; |
| Aig_Man_t * pWnd, * pNew; |
| Aig_Obj_t * pPivot; |
| pPivot = Saig_ManFindPivot( p ); |
| assert( pPivot != NULL ); |
| pWnd = Saig_ManWindowExtract( p, pPivot, nDist ); |
| pNew = Saig_ManWindowInsert( p, pPivot, nDist, pWnd ); |
| Aig_ManStop( pWnd ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collects the nodes that are not linked to each other.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Ptr_t * Saig_ManCollectedDiffNodes( Aig_Man_t * p0, Aig_Man_t * p1 ) |
| { |
| Vec_Ptr_t * vNodes; |
| Aig_Obj_t * pObj0, * pObj1; |
| int i; |
| // collect nodes that are not linked |
| Aig_ManIncrementTravId( p0 ); |
| vNodes = Vec_PtrAlloc( 1000 ); |
| Aig_ManForEachObj( p0, pObj0, i ) |
| { |
| pObj1 = Aig_ObjRepr( p0, pObj0 ); |
| if ( pObj1 != NULL ) |
| { |
| assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) ); |
| continue; |
| } |
| // mark and collect unmatched objects |
| Aig_ObjSetTravIdCurrent( p0, pObj0 ); |
| if ( Aig_ObjIsNode(pObj0) || Aig_ObjIsCi(pObj0) ) |
| Vec_PtrPush( vNodes, pObj0 ); |
| } |
| // make sure LI/LO are labeled/unlabeled mutually |
| Saig_ManForEachLiLo( p0, pObj0, pObj1, i ) |
| assert( Aig_ObjIsTravIdCurrent(p0, pObj0) == |
| Aig_ObjIsTravIdCurrent(p0, pObj1) ); |
| return vNodes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates PIs of the miter.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Saig_ManWindowCreatePis( Aig_Man_t * pNew, Aig_Man_t * p0, Aig_Man_t * p1, Vec_Ptr_t * vNodes0 ) |
| { |
| Aig_Obj_t * pObj, * pMatch, * pFanin; |
| int i, Counter = 0; |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pObj, i ) |
| { |
| if ( Saig_ObjIsLo(p0, pObj) ) |
| { |
| pMatch = Saig_ObjLoToLi( p0, pObj ); |
| pFanin = Aig_ObjFanin0(pMatch); |
| if ( !Aig_ObjIsTravIdCurrent(p0, pFanin) && pFanin->pData == NULL ) |
| { |
| pFanin->pData = Aig_ObjCreateCi(pNew); |
| pMatch = Aig_ObjRepr( p0, pFanin ); |
| assert( pFanin == Aig_ObjRepr( p1, pMatch ) ); |
| assert( pMatch != NULL ); |
| pMatch->pData = pFanin->pData; |
| Counter++; |
| } |
| } |
| else |
| { |
| assert( Aig_ObjIsNode(pObj) ); |
| pFanin = Aig_ObjFanin0(pObj); |
| if ( !Aig_ObjIsTravIdCurrent(p0, pFanin) && pFanin->pData == NULL ) |
| { |
| pFanin->pData = Aig_ObjCreateCi(pNew); |
| pMatch = Aig_ObjRepr( p0, pFanin ); |
| assert( pFanin == Aig_ObjRepr( p1, pMatch ) ); |
| assert( pMatch != NULL ); |
| pMatch->pData = pFanin->pData; |
| Counter++; |
| } |
| pFanin = Aig_ObjFanin1(pObj); |
| if ( !Aig_ObjIsTravIdCurrent(p0, pFanin) && pFanin->pData == NULL ) |
| { |
| pFanin->pData = Aig_ObjCreateCi(pNew); |
| pMatch = Aig_ObjRepr( p0, pFanin ); |
| assert( pFanin == Aig_ObjRepr( p1, pMatch ) ); |
| assert( pMatch != NULL ); |
| pMatch->pData = pFanin->pData; |
| Counter++; |
| } |
| } |
| } |
| // printf( "Added %d primary inputs.\n", Counter ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates POs of the miter.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Saig_ManWindowCreatePos( Aig_Man_t * pNew, Aig_Man_t * p0, Aig_Man_t * p1 ) |
| { |
| Aig_Obj_t * pObj0, * pObj1, * pMiter; |
| Aig_Obj_t * pFanin0, * pFanin1; |
| int i; |
| Aig_ManForEachObj( p0, pObj0, i ) |
| { |
| if ( Aig_ObjIsTravIdCurrent(p0, pObj0) ) |
| continue; |
| if ( Aig_ObjIsConst1(pObj0) ) |
| continue; |
| if ( Aig_ObjIsCi(pObj0) ) |
| continue; |
| pObj1 = Aig_ObjRepr( p0, pObj0 ); |
| assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) ); |
| if ( Aig_ObjIsCo(pObj0) ) |
| { |
| pFanin0 = Aig_ObjFanin0(pObj0); |
| pFanin1 = Aig_ObjFanin0(pObj1); |
| assert( Aig_ObjIsTravIdCurrent(p0, pFanin0) == |
| Aig_ObjIsTravIdCurrent(p1, pFanin1) ); |
| if ( Aig_ObjIsTravIdCurrent(p0, pFanin0) ) |
| { |
| pMiter = Aig_Exor( pNew, (Aig_Obj_t *)pFanin0->pData, (Aig_Obj_t *)pFanin1->pData ); |
| Aig_ObjCreateCo( pNew, pMiter ); |
| } |
| } |
| else |
| { |
| assert( Aig_ObjIsNode(pObj0) ); |
| |
| pFanin0 = Aig_ObjFanin0(pObj0); |
| pFanin1 = Aig_ObjFanin0(pObj1); |
| assert( Aig_ObjIsTravIdCurrent(p0, pFanin0) == |
| Aig_ObjIsTravIdCurrent(p1, pFanin1) ); |
| if ( Aig_ObjIsTravIdCurrent(p0, pFanin0) ) |
| { |
| pMiter = Aig_Exor( pNew, (Aig_Obj_t *)pFanin0->pData, (Aig_Obj_t *)pFanin1->pData ); |
| Aig_ObjCreateCo( pNew, pMiter ); |
| } |
| |
| pFanin0 = Aig_ObjFanin1(pObj0); |
| pFanin1 = Aig_ObjFanin1(pObj1); |
| assert( Aig_ObjIsTravIdCurrent(p0, pFanin0) == |
| Aig_ObjIsTravIdCurrent(p1, pFanin1) ); |
| if ( Aig_ObjIsTravIdCurrent(p0, pFanin0) ) |
| { |
| pMiter = Aig_Exor( pNew, (Aig_Obj_t *)pFanin0->pData, (Aig_Obj_t *)pFanin1->pData ); |
| Aig_ObjCreateCo( pNew, pMiter ); |
| } |
| } |
| } |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Extracts the window AIG from the AIG manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManWindowExtractMiter( Aig_Man_t * p0, Aig_Man_t * p1 ) |
| { |
| Aig_Man_t * pNew; |
| Aig_Obj_t * pObj0, * pObj1, * pMatch0, * pMatch1; |
| Vec_Ptr_t * vNodes0, * vNodes1; |
| int i, nRegCount; |
| // add matching of POs and LIs |
| Saig_ManForEachPo( p0, pObj0, i ) |
| { |
| pObj1 = Aig_ManCo( p1, i ); |
| Aig_ObjSetRepr( p0, pObj0, pObj1 ); |
| Aig_ObjSetRepr( p1, pObj1, pObj0 ); |
| } |
| Saig_ManForEachLi( p0, pObj0, i ) |
| { |
| pMatch0 = Saig_ObjLiToLo( p0, pObj0 ); |
| pMatch1 = Aig_ObjRepr( p0, pMatch0 ); |
| if ( pMatch1 == NULL ) |
| continue; |
| assert( pMatch0 == Aig_ObjRepr( p1, pMatch1 ) ); |
| pObj1 = Saig_ObjLoToLi( p1, pMatch1 ); |
| Aig_ObjSetRepr( p0, pObj0, pObj1 ); |
| Aig_ObjSetRepr( p1, pObj1, pObj0 ); |
| } |
| // clean the markings |
| Aig_ManCleanData( p0 ); |
| Aig_ManCleanData( p1 ); |
| // collect nodes that are not linked |
| vNodes0 = Saig_ManCollectedDiffNodes( p0, p1 ); |
| vNodes1 = Saig_ManCollectedDiffNodes( p1, p0 ); |
| // create the new manager |
| pNew = Aig_ManStart( Vec_PtrSize(vNodes0) + Vec_PtrSize(vNodes1) ); |
| pNew->pName = Abc_UtilStrsav( "wnd" ); |
| pNew->pSpec = NULL; |
| // map constant nodes |
| pObj0 = Aig_ManConst1( p0 ); |
| pObj0->pData = Aig_ManConst1( pNew ); |
| pObj1 = Aig_ManConst1( p1 ); |
| pObj1->pData = Aig_ManConst1( pNew ); |
| // create real PIs |
| Saig_ManWindowCreatePis( pNew, p0, p1, vNodes0 ); |
| Saig_ManWindowCreatePis( pNew, p1, p0, vNodes1 ); |
| // create register outputs |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pObj0, i ) |
| { |
| if ( Saig_ObjIsLo(p0, pObj0) ) |
| pObj0->pData = Aig_ObjCreateCi(pNew); |
| } |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pObj1, i ) |
| { |
| if ( Saig_ObjIsLo(p1, pObj1) ) |
| pObj1->pData = Aig_ObjCreateCi(pNew); |
| } |
| // create internal nodes |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pObj0, i ) |
| { |
| if ( Aig_ObjIsNode(pObj0) ) |
| pObj0->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj0), Aig_ObjChild1Copy(pObj0) ); |
| } |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pObj1, i ) |
| { |
| if ( Aig_ObjIsNode(pObj1) ) |
| pObj1->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj1), Aig_ObjChild1Copy(pObj1) ); |
| } |
| // create POs |
| Saig_ManWindowCreatePos( pNew, p0, p1 ); |
| // Saig_ManWindowCreatePos( pNew, p1, p0 ); |
| // create register inputs |
| nRegCount = 0; |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pObj0, i ) |
| { |
| if ( Saig_ObjIsLo(p0, pObj0) ) |
| { |
| pMatch0 = Saig_ObjLoToLi( p0, pObj0 ); |
| Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch0) ); |
| nRegCount++; |
| } |
| } |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pObj1, i ) |
| { |
| if ( Saig_ObjIsLo(p1, pObj1) ) |
| { |
| pMatch1 = Saig_ObjLoToLi( p1, pObj1 ); |
| Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch1) ); |
| nRegCount++; |
| } |
| } |
| Aig_ManSetRegNum( pNew, nRegCount ); |
| Aig_ManCleanup( pNew ); |
| Vec_PtrFree( vNodes0 ); |
| Vec_PtrFree( vNodes1 ); |
| return pNew; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |