diff options
Diffstat (limited to 'src/aig/ivy/ivyUtil.c')
| -rw-r--r-- | src/aig/ivy/ivyUtil.c | 818 |
1 files changed, 818 insertions, 0 deletions
diff --git a/src/aig/ivy/ivyUtil.c b/src/aig/ivy/ivyUtil.c new file mode 100644 index 00000000..ab62a276 --- /dev/null +++ b/src/aig/ivy/ivyUtil.c @@ -0,0 +1,818 @@ +/**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" + +//////////////////////////////////////////////////////////////////////// +/// 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" ); +} + +/**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 /// +//////////////////////////////////////////////////////////////////////// + + |