| /**CFile**************************************************************** |
| |
| FileName [ivyUtil.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [And-Inverter Graph package.] |
| |
| Synopsis [Various procedures.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - May 11, 2006.] |
| |
| Revision [$Id: ivyUtil.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "ivy.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Increments the current traversal ID of the network.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ivy_ManIncrementTravId( Ivy_Man_t * p ) |
| { |
| if ( p->nTravIds >= (1<<30)-1 - 1000 ) |
| Ivy_ManCleanTravId( p ); |
| p->nTravIds++; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Sets the DFS ordering of the nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ivy_ManCleanTravId( Ivy_Man_t * p ) |
| { |
| Ivy_Obj_t * pObj; |
| int i; |
| p->nTravIds = 1; |
| Ivy_ManForEachObj( p, pObj, i ) |
| pObj->TravId = 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes truth table of the cut.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ivy_ManCollectCut_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vNodes ) |
| { |
| if ( pNode->fMarkA ) |
| return; |
| pNode->fMarkA = 1; |
| assert( Ivy_ObjIsAnd(pNode) || Ivy_ObjIsExor(pNode) ); |
| Ivy_ManCollectCut_rec( p, Ivy_ObjFanin0(pNode), vNodes ); |
| Ivy_ManCollectCut_rec( p, Ivy_ObjFanin1(pNode), vNodes ); |
| Vec_IntPush( vNodes, pNode->Id ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes truth table of the cut.] |
| |
| Description [Does not modify the array of leaves. Uses array vTruth to store |
| temporary truth tables. The returned pointer should be used immediately.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ivy_ManCollectCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes ) |
| { |
| int i, Leaf; |
| // collect and mark the leaves |
| Vec_IntClear( vNodes ); |
| Vec_IntForEachEntry( vLeaves, Leaf, i ) |
| { |
| Vec_IntPush( vNodes, Leaf ); |
| Ivy_ManObj(p, Leaf)->fMarkA = 1; |
| } |
| // collect and mark the nodes |
| Ivy_ManCollectCut_rec( p, pRoot, vNodes ); |
| // clean the nodes |
| Vec_IntForEachEntry( vNodes, Leaf, i ) |
| Ivy_ManObj(p, Leaf)->fMarkA = 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the pointer to the truth table.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| unsigned * Ivy_ObjGetTruthStore( int ObjNum, Vec_Int_t * vTruth ) |
| { |
| return ((unsigned *)Vec_IntArray(vTruth)) + 8 * ObjNum; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes truth table of the cut.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ivy_ManCutTruthOne( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vTruth, int nWords ) |
| { |
| unsigned * pTruth, * pTruth0, * pTruth1; |
| int i; |
| pTruth = Ivy_ObjGetTruthStore( pNode->TravId, vTruth ); |
| pTruth0 = Ivy_ObjGetTruthStore( Ivy_ObjFanin0(pNode)->TravId, vTruth ); |
| pTruth1 = Ivy_ObjGetTruthStore( Ivy_ObjFanin1(pNode)->TravId, vTruth ); |
| if ( Ivy_ObjIsExor(pNode) ) |
| for ( i = 0; i < nWords; i++ ) |
| pTruth[i] = pTruth0[i] ^ pTruth1[i]; |
| else if ( !Ivy_ObjFaninC0(pNode) && !Ivy_ObjFaninC1(pNode) ) |
| for ( i = 0; i < nWords; i++ ) |
| pTruth[i] = pTruth0[i] & pTruth1[i]; |
| else if ( !Ivy_ObjFaninC0(pNode) && Ivy_ObjFaninC1(pNode) ) |
| for ( i = 0; i < nWords; i++ ) |
| pTruth[i] = pTruth0[i] & ~pTruth1[i]; |
| else if ( Ivy_ObjFaninC0(pNode) && !Ivy_ObjFaninC1(pNode) ) |
| for ( i = 0; i < nWords; i++ ) |
| pTruth[i] = ~pTruth0[i] & pTruth1[i]; |
| else // if ( Ivy_ObjFaninC0(pNode) && Ivy_ObjFaninC1(pNode) ) |
| for ( i = 0; i < nWords; i++ ) |
| pTruth[i] = ~pTruth0[i] & ~pTruth1[i]; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes truth table of the cut.] |
| |
| Description [Does not modify the array of leaves. Uses array vTruth to store |
| temporary truth tables. The returned pointer should be used immediately.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| unsigned * Ivy_ManCutTruth( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth ) |
| { |
| static unsigned uTruths[8][8] = { // elementary truth tables |
| { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA }, |
| { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC }, |
| { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 }, |
| { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 }, |
| { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, |
| { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, |
| { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, |
| { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } |
| }; |
| int i, Leaf; |
| // collect the cut |
| Ivy_ManCollectCut( p, pRoot, vLeaves, vNodes ); |
| // set the node numbers |
| Vec_IntForEachEntry( vNodes, Leaf, i ) |
| Ivy_ManObj(p, Leaf)->TravId = i; |
| // alloc enough memory |
| Vec_IntClear( vTruth ); |
| Vec_IntGrow( vTruth, 8 * Vec_IntSize(vNodes) ); |
| // set the elementary truth tables |
| Vec_IntForEachEntry( vLeaves, Leaf, i ) |
| memcpy( Ivy_ObjGetTruthStore(i, vTruth), uTruths[i], 8 * sizeof(unsigned) ); |
| // compute truths for other nodes |
| Vec_IntForEachEntryStart( vNodes, Leaf, i, Vec_IntSize(vLeaves) ) |
| Ivy_ManCutTruthOne( p, Ivy_ManObj(p, Leaf), vTruth, 8 ); |
| return Ivy_ObjGetTruthStore( pRoot->TravId, vTruth ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collect the latches.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p ) |
| { |
| Vec_Int_t * vLatches; |
| Ivy_Obj_t * pObj; |
| int i; |
| vLatches = Vec_IntAlloc( Ivy_ManLatchNum(p) ); |
| Ivy_ManForEachLatch( p, pObj, i ) |
| Vec_IntPush( vLatches, pObj->Id ); |
| return vLatches; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collect the latches.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ivy_ManLevels( Ivy_Man_t * p ) |
| { |
| Ivy_Obj_t * pObj; |
| int i, LevelMax = 0; |
| Ivy_ManForEachPo( p, pObj, i ) |
| LevelMax = IVY_MAX( LevelMax, (int)Ivy_ObjFanin0(pObj)->Level ); |
| return LevelMax; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collect the latches.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ivy_ManResetLevels_rec( Ivy_Obj_t * pObj ) |
| { |
| if ( pObj->Level || Ivy_ObjIsCi(pObj) || Ivy_ObjIsConst1(pObj) ) |
| return pObj->Level; |
| if ( Ivy_ObjIsBuf(pObj) ) |
| return pObj->Level = Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) ); |
| assert( Ivy_ObjIsNode(pObj) ); |
| Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) ); |
| Ivy_ManResetLevels_rec( Ivy_ObjFanin1(pObj) ); |
| return pObj->Level = Ivy_ObjLevelNew( pObj ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collect the latches.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ivy_ManResetLevels( Ivy_Man_t * p ) |
| { |
| Ivy_Obj_t * pObj; |
| int i; |
| Ivy_ManForEachObj( p, pObj, i ) |
| pObj->Level = 0; |
| Ivy_ManForEachCo( p, pObj, i ) |
| Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [References/references the node and returns MFFC size.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ivy_ObjRefDeref( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fReference, int fLabel ) |
| { |
| Ivy_Obj_t * pNode0, * pNode1; |
| int Counter; |
| // label visited nodes |
| if ( fLabel ) |
| Ivy_ObjSetTravIdCurrent( p, pNode ); |
| // skip the CI |
| if ( Ivy_ObjIsPi(pNode) ) |
| return 0; |
| assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) || Ivy_ObjIsLatch(pNode) ); |
| // process the internal node |
| pNode0 = Ivy_ObjFanin0(pNode); |
| pNode1 = Ivy_ObjFanin1(pNode); |
| Counter = Ivy_ObjIsNode(pNode); |
| if ( fReference ) |
| { |
| if ( pNode0->nRefs++ == 0 ) |
| Counter += Ivy_ObjRefDeref( p, pNode0, fReference, fLabel ); |
| if ( pNode1 && pNode1->nRefs++ == 0 ) |
| Counter += Ivy_ObjRefDeref( p, pNode1, fReference, fLabel ); |
| } |
| else |
| { |
| assert( pNode0->nRefs > 0 ); |
| assert( pNode1 == NULL || pNode1->nRefs > 0 ); |
| if ( --pNode0->nRefs == 0 ) |
| Counter += Ivy_ObjRefDeref( p, pNode0, fReference, fLabel ); |
| if ( pNode1 && --pNode1->nRefs == 0 ) |
| Counter += Ivy_ObjRefDeref( p, pNode1, fReference, fLabel ); |
| } |
| return Counter; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Labels MFFC with the current label.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ivy_ObjMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pNode ) |
| { |
| int nConeSize1, nConeSize2; |
| assert( !Ivy_IsComplement( pNode ) ); |
| assert( Ivy_ObjIsNode( pNode ) ); |
| nConeSize1 = Ivy_ObjRefDeref( p, pNode, 0, 1 ); // dereference |
| nConeSize2 = Ivy_ObjRefDeref( p, pNode, 1, 0 ); // reference |
| assert( nConeSize1 == nConeSize2 ); |
| assert( nConeSize1 > 0 ); |
| return nConeSize1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Recursively updates fanout levels.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ivy_ObjUpdateLevel_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj ) |
| { |
| Ivy_Obj_t * pFanout; |
| Vec_Ptr_t * vFanouts; |
| int i, LevelNew; |
| assert( p->fFanout ); |
| assert( Ivy_ObjIsNode(pObj) ); |
| vFanouts = Vec_PtrAlloc( 10 ); |
| Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i ) |
| { |
| if ( Ivy_ObjIsCo(pFanout) ) |
| { |
| // assert( (int)Ivy_ObjFanin0(pFanout)->Level <= p->nLevelMax ); |
| continue; |
| } |
| LevelNew = Ivy_ObjLevelNew( pFanout ); |
| if ( (int)pFanout->Level == LevelNew ) |
| continue; |
| pFanout->Level = LevelNew; |
| Ivy_ObjUpdateLevel_rec( p, pFanout ); |
| } |
| Vec_PtrFree( vFanouts ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Compute the new required level.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ivy_ObjLevelRNew( Ivy_Man_t * p, Ivy_Obj_t * pObj ) |
| { |
| Ivy_Obj_t * pFanout; |
| Vec_Ptr_t * vFanouts; |
| int i, Required, LevelNew = 1000000; |
| assert( p->fFanout && p->vRequired ); |
| vFanouts = Vec_PtrAlloc( 10 ); |
| Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i ) |
| { |
| Required = Vec_IntEntry(p->vRequired, pFanout->Id); |
| LevelNew = IVY_MIN( LevelNew, Required ); |
| } |
| Vec_PtrFree( vFanouts ); |
| return LevelNew - 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Recursively updates fanout levels.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ivy_ObjUpdateLevelR_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ReqNew ) |
| { |
| Ivy_Obj_t * pFanin; |
| if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) ) |
| return; |
| assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) ); |
| // process the first fanin |
| pFanin = Ivy_ObjFanin0(pObj); |
| if ( Vec_IntEntry(p->vRequired, pFanin->Id) > ReqNew - 1 ) |
| { |
| Vec_IntWriteEntry( p->vRequired, pFanin->Id, ReqNew - 1 ); |
| Ivy_ObjUpdateLevelR_rec( p, pFanin, ReqNew - 1 ); |
| } |
| if ( Ivy_ObjIsBuf(pObj) ) |
| return; |
| // process the second fanin |
| pFanin = Ivy_ObjFanin1(pObj); |
| if ( Vec_IntEntry(p->vRequired, pFanin->Id) > ReqNew - 1 ) |
| { |
| Vec_IntWriteEntry( p->vRequired, pFanin->Id, ReqNew - 1 ); |
| Ivy_ObjUpdateLevelR_rec( p, pFanin, ReqNew - 1 ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ivy_ObjIsMuxType( Ivy_Obj_t * pNode ) |
| { |
| Ivy_Obj_t * pNode0, * pNode1; |
| // check that the node is regular |
| assert( !Ivy_IsComplement(pNode) ); |
| // if the node is not AND, this is not MUX |
| if ( !Ivy_ObjIsAnd(pNode) ) |
| return 0; |
| // if the children are not complemented, this is not MUX |
| if ( !Ivy_ObjFaninC0(pNode) || !Ivy_ObjFaninC1(pNode) ) |
| return 0; |
| // get children |
| pNode0 = Ivy_ObjFanin0(pNode); |
| pNode1 = Ivy_ObjFanin1(pNode); |
| // if the children are not ANDs, this is not MUX |
| if ( !Ivy_ObjIsAnd(pNode0) || !Ivy_ObjIsAnd(pNode1) ) |
| return 0; |
| // otherwise the node is MUX iff it has a pair of equal grandchildren |
| return (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || |
| (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1))) || |
| (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || |
| (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1))); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Recognizes what nodes are control and data inputs of a MUX.] |
| |
| Description [If the node is a MUX, returns the control variable C. |
| Assigns nodes T and E to be the then and else variables of the MUX. |
| Node C is never complemented. Nodes T and E can be complemented. |
| This function also recognizes EXOR/NEXOR gates as MUXes.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pNode, Ivy_Obj_t ** ppNodeT, Ivy_Obj_t ** ppNodeE ) |
| { |
| Ivy_Obj_t * pNode0, * pNode1; |
| assert( !Ivy_IsComplement(pNode) ); |
| assert( Ivy_ObjIsMuxType(pNode) ); |
| // get children |
| pNode0 = Ivy_ObjFanin0(pNode); |
| pNode1 = Ivy_ObjFanin1(pNode); |
| // find the control variable |
| // if ( pNode1->p1 == Fraig_Not(pNode2->p1) ) |
| if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1)) ) |
| { |
| // if ( Fraig_IsComplement(pNode1->p1) ) |
| if ( Ivy_ObjFaninC0(pNode0) ) |
| { // pNode2->p1 is positive phase of C |
| *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); |
| *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); |
| return Ivy_ObjChild0(pNode1);//pNode2->p1; |
| } |
| else |
| { // pNode1->p1 is positive phase of C |
| *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); |
| *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); |
| return Ivy_ObjChild0(pNode0);//pNode1->p1; |
| } |
| } |
| // else if ( pNode1->p1 == Fraig_Not(pNode2->p2) ) |
| else if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1)) ) |
| { |
| // if ( Fraig_IsComplement(pNode1->p1) ) |
| if ( Ivy_ObjFaninC0(pNode0) ) |
| { // pNode2->p2 is positive phase of C |
| *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); |
| *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); |
| return Ivy_ObjChild1(pNode1);//pNode2->p2; |
| } |
| else |
| { // pNode1->p1 is positive phase of C |
| *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); |
| *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); |
| return Ivy_ObjChild0(pNode0);//pNode1->p1; |
| } |
| } |
| // else if ( pNode1->p2 == Fraig_Not(pNode2->p1) ) |
| else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1)) ) |
| { |
| // if ( Fraig_IsComplement(pNode1->p2) ) |
| if ( Ivy_ObjFaninC1(pNode0) ) |
| { // pNode2->p1 is positive phase of C |
| *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); |
| *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); |
| return Ivy_ObjChild0(pNode1);//pNode2->p1; |
| } |
| else |
| { // pNode1->p2 is positive phase of C |
| *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); |
| *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); |
| return Ivy_ObjChild1(pNode0);//pNode1->p2; |
| } |
| } |
| // else if ( pNode1->p2 == Fraig_Not(pNode2->p2) ) |
| else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)) ) |
| { |
| // if ( Fraig_IsComplement(pNode1->p2) ) |
| if ( Ivy_ObjFaninC1(pNode0) ) |
| { // pNode2->p2 is positive phase of C |
| *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); |
| *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); |
| return Ivy_ObjChild1(pNode1);//pNode2->p2; |
| } |
| else |
| { // pNode1->p2 is positive phase of C |
| *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); |
| *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); |
| return Ivy_ObjChild1(pNode0);//pNode1->p2; |
| } |
| } |
| assert( 0 ); // this is not MUX |
| return NULL; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the real fanin.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj ) |
| { |
| Ivy_Obj_t * pFanin; |
| if ( pObj == NULL || !Ivy_ObjIsBuf( Ivy_Regular(pObj) ) ) |
| return pObj; |
| pFanin = Ivy_ObjReal( Ivy_ObjChild0(Ivy_Regular(pObj)) ); |
| return Ivy_NotCond( pFanin, Ivy_IsComplement(pObj) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Prints node in HAIG.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ivy_ObjPrintVerbose( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fHaig ) |
| { |
| Ivy_Obj_t * pTemp; |
| int fShowFanouts = 0; |
| assert( !Ivy_IsComplement(pObj) ); |
| printf( "Node %5d : ", Ivy_ObjId(pObj) ); |
| if ( Ivy_ObjIsConst1(pObj) ) |
| printf( "constant 1" ); |
| else if ( Ivy_ObjIsPi(pObj) ) |
| printf( "PI" ); |
| else if ( Ivy_ObjIsPo(pObj) ) |
| printf( "PO" ); |
| else if ( Ivy_ObjIsLatch(pObj) ) |
| printf( "latch (%d%s)", Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") ); |
| else if ( Ivy_ObjIsBuf(pObj) ) |
| printf( "buffer (%d%s)", Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") ); |
| else |
| printf( "AND( %5d%s, %5d%s )", |
| Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " "), |
| Ivy_ObjFanin1(pObj)->Id, (Ivy_ObjFaninC1(pObj)? "\'" : " ") ); |
| printf( " (refs = %3d)", Ivy_ObjRefs(pObj) ); |
| if ( fShowFanouts ) |
| { |
| Vec_Ptr_t * vFanouts; |
| Ivy_Obj_t * pFanout; |
| int i; |
| vFanouts = Vec_PtrAlloc( 10 ); |
| printf( "\nFanouts:\n" ); |
| Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i ) |
| { |
| printf( " " ); |
| printf( "Node %5d : ", Ivy_ObjId(pFanout) ); |
| if ( Ivy_ObjIsPo(pFanout) ) |
| printf( "PO" ); |
| else if ( Ivy_ObjIsLatch(pFanout) ) |
| printf( "latch (%d%s)", Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " ") ); |
| else if ( Ivy_ObjIsBuf(pFanout) ) |
| printf( "buffer (%d%s)", Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " ") ); |
| else |
| printf( "AND( %5d%s, %5d%s )", |
| Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " "), |
| Ivy_ObjFanin1(pFanout)->Id, (Ivy_ObjFaninC1(pFanout)? "\'" : " ") ); |
| printf( "\n" ); |
| } |
| Vec_PtrFree( vFanouts ); |
| return; |
| } |
| if ( !fHaig ) |
| { |
| if ( pObj->pEquiv == NULL ) |
| printf( " HAIG node not given" ); |
| else |
| printf( " HAIG node = %d%s", Ivy_Regular(pObj->pEquiv)->Id, (Ivy_IsComplement(pObj->pEquiv)? "\'" : " ") ); |
| return; |
| } |
| if ( pObj->pEquiv == NULL ) |
| return; |
| // there are choices |
| if ( Ivy_ObjRefs(pObj) > 0 ) |
| { |
| // print equivalence class |
| printf( " { %5d ", pObj->Id ); |
| assert( !Ivy_IsComplement(pObj->pEquiv) ); |
| for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) ) |
| printf( " %5d%s", pTemp->Id, (Ivy_IsComplement(pTemp->pEquiv)? "\'" : " ") ); |
| printf( " }" ); |
| return; |
| } |
| // this is a secondary node |
| for ( pTemp = Ivy_Regular(pObj->pEquiv); Ivy_ObjRefs(pTemp) == 0; pTemp = Ivy_Regular(pTemp->pEquiv) ); |
| assert( Ivy_ObjRefs(pTemp) > 0 ); |
| printf( " class of %d", pTemp->Id ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Prints node in HAIG.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig ) |
| { |
| Vec_Int_t * vNodes; |
| Ivy_Obj_t * pObj; |
| int i; |
| printf( "PIs: " ); |
| Ivy_ManForEachPi( p, pObj, i ) |
| printf( " %d", pObj->Id ); |
| printf( "\n" ); |
| printf( "POs: " ); |
| Ivy_ManForEachPo( p, pObj, i ) |
| printf( " %d", pObj->Id ); |
| printf( "\n" ); |
| printf( "Latches: " ); |
| Ivy_ManForEachLatch( p, pObj, i ) |
| printf( " %d=%d%s", pObj->Id, Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") ); |
| printf( "\n" ); |
| vNodes = Ivy_ManDfsSeq( p, NULL ); |
| Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) |
| Ivy_ObjPrintVerbose( p, pObj, fHaig ), printf( "\n" ); |
| printf( "\n" ); |
| Vec_IntFree( vNodes ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs incremental rewriting of the AIG.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ivy_CutTruthPrint2( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth ) |
| { |
| int i; |
| printf( "Trying cut : {" ); |
| for ( i = 0; i < pCut->nSize; i++ ) |
| printf( " %6d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) ); |
| printf( " } " ); |
| Extra_PrintBinary( stdout, &uTruth, 16 ); printf( "\n" ); |
| return 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs incremental rewriting of the AIG.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ivy_CutTruthPrint( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth ) |
| { |
| Vec_Ptr_t * vArray; |
| Ivy_Obj_t * pObj, * pFanout; |
| int nLatches = 0; |
| int nPresent = 0; |
| int i, k; |
| int fVerbose = 0; |
| |
| if ( fVerbose ) |
| printf( "Trying cut : {" ); |
| for ( i = 0; i < pCut->nSize; i++ ) |
| { |
| if ( fVerbose ) |
| printf( " %6d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) ); |
| nLatches += Ivy_LeafLat(pCut->pArray[i]); |
| } |
| if ( fVerbose ) |
| printf( " } " ); |
| if ( fVerbose ) |
| printf( "Latches = %d. ", nLatches ); |
| |
| // check if there are latches on the fanout edges |
| vArray = Vec_PtrAlloc( 100 ); |
| for ( i = 0; i < pCut->nSize; i++ ) |
| { |
| pObj = Ivy_ManObj( p, Ivy_LeafId(pCut->pArray[i]) ); |
| Ivy_ObjForEachFanout( p, pObj, vArray, pFanout, k ) |
| { |
| if ( Ivy_ObjIsLatch(pFanout) ) |
| { |
| nPresent++; |
| break; |
| } |
| } |
| } |
| Vec_PtrSize( vArray ); |
| if ( fVerbose ) |
| { |
| printf( "Present = %d. ", nPresent ); |
| if ( nLatches > nPresent ) |
| printf( "Clauses = %d. ", 2*(nLatches - nPresent) ); |
| printf( "\n" ); |
| } |
| return ( nLatches > nPresent ) ? 2*(nLatches - nPresent) : 0; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
