abc70930: src/aig/ivy/ivyUtil.c Source File

00001 
00021 #include "ivy.h"
00022 
00026 
00030 
00042 void Ivy_ManIncrementTravId( Ivy_Man_t * p )
00043 {
00044     if ( p->nTravIds >= (1<<30)-1 - 1000 )
00045         Ivy_ManCleanTravId( p );
00046     p->nTravIds++;
00047 }
00048 
00060 void Ivy_ManCleanTravId( Ivy_Man_t * p )
00061 {
00062     Ivy_Obj_t * pObj;
00063     int i;
00064     p->nTravIds = 1;
00065     Ivy_ManForEachObj( p, pObj, i )
00066         pObj->TravId = 0;
00067 }
00068 
00080 void Ivy_ManCollectCut_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vNodes )
00081 {
00082     if ( pNode->fMarkA )
00083         return;
00084     pNode->fMarkA = 1;
00085     assert( Ivy_ObjIsAnd(pNode) || Ivy_ObjIsExor(pNode) );
00086     Ivy_ManCollectCut_rec( p, Ivy_ObjFanin0(pNode), vNodes );
00087     Ivy_ManCollectCut_rec( p, Ivy_ObjFanin1(pNode), vNodes );
00088     Vec_IntPush( vNodes, pNode->Id );
00089 }
00090 
00103 void Ivy_ManCollectCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
00104 {
00105     int i, Leaf;
00106     // collect and mark the leaves
00107     Vec_IntClear( vNodes );
00108     Vec_IntForEachEntry( vLeaves, Leaf, i )
00109     {
00110         Vec_IntPush( vNodes, Leaf );
00111         Ivy_ManObj(p, Leaf)->fMarkA = 1;
00112     }
00113     // collect and mark the nodes
00114     Ivy_ManCollectCut_rec( p, pRoot, vNodes );
00115     // clean the nodes
00116     Vec_IntForEachEntry( vNodes, Leaf, i )
00117         Ivy_ManObj(p, Leaf)->fMarkA = 0;
00118 }
00119 
00131 unsigned * Ivy_ObjGetTruthStore( int ObjNum, Vec_Int_t * vTruth )
00132 {
00133    return ((unsigned *)Vec_IntArray(vTruth)) + 8 * ObjNum;
00134 }
00135 
00147 void Ivy_ManCutTruthOne( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vTruth, int nWords )
00148 {
00149     unsigned * pTruth, * pTruth0, * pTruth1;
00150     int i;
00151     pTruth  = Ivy_ObjGetTruthStore( pNode->TravId, vTruth );
00152     pTruth0 = Ivy_ObjGetTruthStore( Ivy_ObjFanin0(pNode)->TravId, vTruth );
00153     pTruth1 = Ivy_ObjGetTruthStore( Ivy_ObjFanin1(pNode)->TravId, vTruth );
00154     if ( Ivy_ObjIsExor(pNode) )
00155         for ( i = 0; i < nWords; i++ )
00156             pTruth[i] = pTruth0[i] ^ pTruth1[i];
00157     else if ( !Ivy_ObjFaninC0(pNode) && !Ivy_ObjFaninC1(pNode) )
00158         for ( i = 0; i < nWords; i++ )
00159             pTruth[i] = pTruth0[i] & pTruth1[i];
00160     else if ( !Ivy_ObjFaninC0(pNode) && Ivy_ObjFaninC1(pNode) )
00161         for ( i = 0; i < nWords; i++ )
00162             pTruth[i] = pTruth0[i] & ~pTruth1[i];
00163     else if ( Ivy_ObjFaninC0(pNode) && !Ivy_ObjFaninC1(pNode) )
00164         for ( i = 0; i < nWords; i++ )
00165             pTruth[i] = ~pTruth0[i] & pTruth1[i];
00166     else // if ( Ivy_ObjFaninC0(pNode) && Ivy_ObjFaninC1(pNode) )
00167         for ( i = 0; i < nWords; i++ )
00168             pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
00169 }
00170 
00183 unsigned * Ivy_ManCutTruth( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth )
00184 {
00185     static unsigned uTruths[8][8] = { // elementary truth tables
00186         { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
00187         { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
00188         { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
00189         { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
00190         { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
00191         { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 
00192         { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 
00193         { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
00194     };
00195     int i, Leaf;
00196     // collect the cut
00197     Ivy_ManCollectCut( p, pRoot, vLeaves, vNodes );
00198     // set the node numbers
00199     Vec_IntForEachEntry( vNodes, Leaf, i )
00200         Ivy_ManObj(p, Leaf)->TravId = i;
00201     // alloc enough memory
00202     Vec_IntClear( vTruth );
00203     Vec_IntGrow( vTruth, 8 * Vec_IntSize(vNodes) );
00204     // set the elementary truth tables
00205     Vec_IntForEachEntry( vLeaves, Leaf, i )
00206         memcpy( Ivy_ObjGetTruthStore(i, vTruth), uTruths[i], 8 * sizeof(unsigned) );
00207     // compute truths for other nodes
00208     Vec_IntForEachEntryStart( vNodes, Leaf, i, Vec_IntSize(vLeaves) )
00209         Ivy_ManCutTruthOne( p, Ivy_ManObj(p, Leaf), vTruth, 8 );
00210     return Ivy_ObjGetTruthStore( pRoot->TravId, vTruth );
00211 }
00212 
00224 Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p )
00225 {
00226     Vec_Int_t * vLatches;
00227     Ivy_Obj_t * pObj;
00228     int i;
00229     vLatches = Vec_IntAlloc( Ivy_ManLatchNum(p) );
00230     Ivy_ManForEachLatch( p, pObj, i )
00231         Vec_IntPush( vLatches, pObj->Id );
00232     return vLatches;
00233 }
00234 
00246 int Ivy_ManLevels( Ivy_Man_t * p )
00247 {
00248     Ivy_Obj_t * pObj;
00249     int i, LevelMax = 0;
00250     Ivy_ManForEachPo( p, pObj, i )
00251         LevelMax = IVY_MAX( LevelMax, (int)Ivy_ObjFanin0(pObj)->Level );
00252     return LevelMax;
00253 }
00254 
00266 int Ivy_ManResetLevels_rec( Ivy_Obj_t * pObj )
00267 {
00268     if ( pObj->Level || Ivy_ObjIsCi(pObj) || Ivy_ObjIsConst1(pObj) )
00269         return pObj->Level;
00270     if ( Ivy_ObjIsBuf(pObj) )
00271         return pObj->Level = Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) );
00272     assert( Ivy_ObjIsNode(pObj) );
00273     Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) );
00274     Ivy_ManResetLevels_rec( Ivy_ObjFanin1(pObj) );
00275     return pObj->Level = Ivy_ObjLevelNew( pObj );
00276 }
00277 
00289 void Ivy_ManResetLevels( Ivy_Man_t * p )
00290 {
00291     Ivy_Obj_t * pObj;
00292     int i;
00293     Ivy_ManForEachObj( p, pObj, i )
00294         pObj->Level = 0;
00295     Ivy_ManForEachCo( p, pObj, i )
00296         Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) );
00297 }
00298 
00310 int Ivy_ObjRefDeref( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fReference, int fLabel )
00311 {
00312     Ivy_Obj_t * pNode0, * pNode1;
00313     int Counter;
00314     // label visited nodes
00315     if ( fLabel )
00316         Ivy_ObjSetTravIdCurrent( p, pNode );
00317     // skip the CI
00318     if ( Ivy_ObjIsPi(pNode) )
00319         return 0;
00320     assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) || Ivy_ObjIsLatch(pNode) );
00321     // process the internal node
00322     pNode0 = Ivy_ObjFanin0(pNode);
00323     pNode1 = Ivy_ObjFanin1(pNode);
00324     Counter = Ivy_ObjIsNode(pNode);
00325     if ( fReference )
00326     {
00327         if ( pNode0->nRefs++ == 0 )
00328             Counter += Ivy_ObjRefDeref( p, pNode0, fReference, fLabel );
00329         if ( pNode1 && pNode1->nRefs++ == 0 )
00330             Counter += Ivy_ObjRefDeref( p, pNode1, fReference, fLabel );
00331     }
00332     else
00333     {
00334         assert( pNode0->nRefs > 0 );
00335         assert( pNode1 == NULL || pNode1->nRefs > 0 );
00336         if ( --pNode0->nRefs == 0 )
00337             Counter += Ivy_ObjRefDeref( p, pNode0, fReference, fLabel );
00338         if ( pNode1 && --pNode1->nRefs == 0 )
00339             Counter += Ivy_ObjRefDeref( p, pNode1, fReference, fLabel );
00340     }
00341     return Counter;
00342 }
00343 
00344 
00356 int Ivy_ObjMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pNode )
00357 {
00358     int nConeSize1, nConeSize2;
00359     assert( !Ivy_IsComplement( pNode ) );
00360     assert( Ivy_ObjIsNode( pNode ) );
00361     nConeSize1 = Ivy_ObjRefDeref( p, pNode, 0, 1 ); // dereference
00362     nConeSize2 = Ivy_ObjRefDeref( p, pNode, 1, 0 ); // reference
00363     assert( nConeSize1 == nConeSize2 );
00364     assert( nConeSize1 > 0 );
00365     return nConeSize1;
00366 }
00367 
00379 void Ivy_ObjUpdateLevel_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj )
00380 {
00381     Ivy_Obj_t * pFanout;
00382     Vec_Ptr_t * vFanouts;
00383     int i, LevelNew;
00384     assert( p->fFanout );
00385     assert( Ivy_ObjIsNode(pObj) );
00386     vFanouts = Vec_PtrAlloc( 10 );
00387     Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i )
00388     {
00389         if ( Ivy_ObjIsCo(pFanout) )
00390         {
00391 //            assert( (int)Ivy_ObjFanin0(pFanout)->Level <= p->nLevelMax );
00392             continue;
00393         }
00394         LevelNew = Ivy_ObjLevelNew( pFanout );
00395         if ( (int)pFanout->Level == LevelNew )
00396             continue;
00397         pFanout->Level = LevelNew;
00398         Ivy_ObjUpdateLevel_rec( p, pFanout );
00399     }
00400     Vec_PtrFree( vFanouts );
00401 }
00402 
00414 int Ivy_ObjLevelRNew( Ivy_Man_t * p, Ivy_Obj_t * pObj )
00415 {
00416     Ivy_Obj_t * pFanout;
00417     Vec_Ptr_t * vFanouts;
00418     int i, Required, LevelNew = 1000000;
00419     assert( p->fFanout && p->vRequired );
00420     vFanouts = Vec_PtrAlloc( 10 );
00421     Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i )
00422     {
00423         Required = Vec_IntEntry(p->vRequired, pFanout->Id);
00424         LevelNew = IVY_MIN( LevelNew, Required );
00425     }
00426     Vec_PtrFree( vFanouts );
00427     return LevelNew - 1;
00428 }
00429 
00441 void Ivy_ObjUpdateLevelR_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ReqNew )
00442 {
00443     Ivy_Obj_t * pFanin;
00444     if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) )
00445         return;
00446     assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) );
00447     // process the first fanin
00448     pFanin = Ivy_ObjFanin0(pObj);
00449     if ( Vec_IntEntry(p->vRequired, pFanin->Id) > ReqNew - 1 )
00450     {
00451         Vec_IntWriteEntry( p->vRequired, pFanin->Id, ReqNew - 1 );
00452         Ivy_ObjUpdateLevelR_rec( p, pFanin, ReqNew - 1 );
00453     }
00454     if ( Ivy_ObjIsBuf(pObj) )
00455         return;
00456     // process the second fanin
00457     pFanin = Ivy_ObjFanin1(pObj);
00458     if ( Vec_IntEntry(p->vRequired, pFanin->Id) > ReqNew - 1 )
00459     {
00460         Vec_IntWriteEntry( p->vRequired, pFanin->Id, ReqNew - 1 );
00461         Ivy_ObjUpdateLevelR_rec( p, pFanin, ReqNew - 1 );
00462     }
00463 }
00464 
00476 int Ivy_ObjIsMuxType( Ivy_Obj_t * pNode )
00477 {
00478     Ivy_Obj_t * pNode0, * pNode1;
00479     // check that the node is regular
00480     assert( !Ivy_IsComplement(pNode) );
00481     // if the node is not AND, this is not MUX
00482     if ( !Ivy_ObjIsAnd(pNode) )
00483         return 0;
00484     // if the children are not complemented, this is not MUX
00485     if ( !Ivy_ObjFaninC0(pNode) || !Ivy_ObjFaninC1(pNode) )
00486         return 0;
00487     // get children
00488     pNode0 = Ivy_ObjFanin0(pNode);
00489     pNode1 = Ivy_ObjFanin1(pNode);
00490     // if the children are not ANDs, this is not MUX
00491     if ( !Ivy_ObjIsAnd(pNode0) || !Ivy_ObjIsAnd(pNode1) )
00492         return 0;
00493     // otherwise the node is MUX iff it has a pair of equal grandchildren
00494     return (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || 
00495            (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1))) ||
00496            (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1))) ||
00497            (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)));
00498 }
00499 
00514 Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pNode, Ivy_Obj_t ** ppNodeT, Ivy_Obj_t ** ppNodeE )
00515 {
00516     Ivy_Obj_t * pNode0, * pNode1;
00517     assert( !Ivy_IsComplement(pNode) );
00518     assert( Ivy_ObjIsMuxType(pNode) );
00519     // get children
00520     pNode0 = Ivy_ObjFanin0(pNode);
00521     pNode1 = Ivy_ObjFanin1(pNode);
00522     // find the control variable
00523 //    if ( pNode1->p1 == Fraig_Not(pNode2->p1) )
00524     if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1)) )
00525     {
00526 //        if ( Fraig_IsComplement(pNode1->p1) )
00527         if ( Ivy_ObjFaninC0(pNode0) )
00528         { // pNode2->p1 is positive phase of C
00529             *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
00530             *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
00531             return Ivy_ObjChild0(pNode1);//pNode2->p1;
00532         }
00533         else
00534         { // pNode1->p1 is positive phase of C
00535             *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
00536             *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
00537             return Ivy_ObjChild0(pNode0);//pNode1->p1;
00538         }
00539     }
00540 //    else if ( pNode1->p1 == Fraig_Not(pNode2->p2) )
00541     else if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1)) )
00542     {
00543 //        if ( Fraig_IsComplement(pNode1->p1) )
00544         if ( Ivy_ObjFaninC0(pNode0) )
00545         { // pNode2->p2 is positive phase of C
00546             *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
00547             *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
00548             return Ivy_ObjChild1(pNode1);//pNode2->p2;
00549         }
00550         else
00551         { // pNode1->p1 is positive phase of C
00552             *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
00553             *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
00554             return Ivy_ObjChild0(pNode0);//pNode1->p1;
00555         }
00556     }
00557 //    else if ( pNode1->p2 == Fraig_Not(pNode2->p1) )
00558     else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1)) )
00559     {
00560 //        if ( Fraig_IsComplement(pNode1->p2) )
00561         if ( Ivy_ObjFaninC1(pNode0) )
00562         { // pNode2->p1 is positive phase of C
00563             *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
00564             *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
00565             return Ivy_ObjChild0(pNode1);//pNode2->p1;
00566         }
00567         else
00568         { // pNode1->p2 is positive phase of C
00569             *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
00570             *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
00571             return Ivy_ObjChild1(pNode0);//pNode1->p2;
00572         }
00573     }
00574 //    else if ( pNode1->p2 == Fraig_Not(pNode2->p2) )
00575     else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)) )
00576     {
00577 //        if ( Fraig_IsComplement(pNode1->p2) )
00578         if ( Ivy_ObjFaninC1(pNode0) )
00579         { // pNode2->p2 is positive phase of C
00580             *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
00581             *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
00582             return Ivy_ObjChild1(pNode1);//pNode2->p2;
00583         }
00584         else
00585         { // pNode1->p2 is positive phase of C
00586             *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
00587             *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
00588             return Ivy_ObjChild1(pNode0);//pNode1->p2;
00589         }
00590     }
00591     assert( 0 ); // this is not MUX
00592     return NULL;
00593 }
00594 
00606 Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj )
00607 {
00608     Ivy_Obj_t * pFanin;
00609     if ( pObj == NULL || !Ivy_ObjIsBuf( Ivy_Regular(pObj) ) )
00610         return pObj;
00611     pFanin = Ivy_ObjReal( Ivy_ObjChild0(Ivy_Regular(pObj)) );
00612     return Ivy_NotCond( pFanin, Ivy_IsComplement(pObj) );
00613 }
00614 
00626 void Ivy_ObjPrintVerbose( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fHaig )
00627 {
00628     Ivy_Obj_t * pTemp;
00629     int fShowFanouts = 0;
00630     assert( !Ivy_IsComplement(pObj) );
00631     printf( "Node %5d : ", Ivy_ObjId(pObj) );
00632     if ( Ivy_ObjIsConst1(pObj) )
00633         printf( "constant 1" );
00634     else if ( Ivy_ObjIsPi(pObj) )
00635         printf( "PI" );
00636     else if ( Ivy_ObjIsPo(pObj) )
00637         printf( "PO" );
00638     else if ( Ivy_ObjIsLatch(pObj) )
00639         printf( "latch (%d%s)", Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
00640     else if ( Ivy_ObjIsBuf(pObj) )
00641         printf( "buffer (%d%s)", Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
00642     else
00643         printf( "AND( %5d%s, %5d%s )", 
00644             Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " "), 
00645             Ivy_ObjFanin1(pObj)->Id, (Ivy_ObjFaninC1(pObj)? "\'" : " ") );
00646     printf( " (refs = %3d)", Ivy_ObjRefs(pObj) );
00647     if ( fShowFanouts )
00648     {
00649         Vec_Ptr_t * vFanouts;
00650         Ivy_Obj_t * pFanout;
00651         int i;
00652         vFanouts = Vec_PtrAlloc( 10 );
00653         printf( "\nFanouts:\n" );
00654         Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i )
00655         {
00656             printf( "    " );
00657             printf( "Node %5d : ", Ivy_ObjId(pFanout) );
00658             if ( Ivy_ObjIsPo(pFanout) )
00659                 printf( "PO" );
00660             else if ( Ivy_ObjIsLatch(pFanout) )
00661                 printf( "latch (%d%s)", Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " ") );
00662             else if ( Ivy_ObjIsBuf(pFanout) )
00663                 printf( "buffer (%d%s)", Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " ") );
00664             else
00665                 printf( "AND( %5d%s, %5d%s )", 
00666                     Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " "), 
00667                     Ivy_ObjFanin1(pFanout)->Id, (Ivy_ObjFaninC1(pFanout)? "\'" : " ") );
00668             printf( "\n" );
00669         }
00670         Vec_PtrFree( vFanouts );
00671         return;
00672     }
00673     if ( !fHaig )
00674     {
00675         if ( pObj->pEquiv == NULL )
00676             printf( " HAIG node not given" );
00677         else
00678             printf( " HAIG node = %d%s", Ivy_Regular(pObj->pEquiv)->Id, (Ivy_IsComplement(pObj->pEquiv)? "\'" : " ") );
00679         return;
00680     }
00681     if ( pObj->pEquiv == NULL )
00682         return;
00683     // there are choices
00684     if ( Ivy_ObjRefs(pObj) > 0 )
00685     {
00686         // print equivalence class
00687         printf( "  { %5d ", pObj->Id );
00688         assert( !Ivy_IsComplement(pObj->pEquiv) );
00689         for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
00690             printf( " %5d%s", pTemp->Id, (Ivy_IsComplement(pTemp->pEquiv)? "\'" : " ") );
00691         printf( " }" );
00692         return;
00693     }
00694     // this is a secondary node
00695     for ( pTemp = Ivy_Regular(pObj->pEquiv); Ivy_ObjRefs(pTemp) == 0; pTemp = Ivy_Regular(pTemp->pEquiv) );
00696     assert( Ivy_ObjRefs(pTemp) > 0 );
00697     printf( "  class of %d", pTemp->Id );
00698 }
00699 
00711 void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig )
00712 {
00713     Vec_Int_t * vNodes;
00714     Ivy_Obj_t * pObj;
00715     int i;
00716     printf( "PIs: " );
00717     Ivy_ManForEachPi( p, pObj, i )
00718         printf( " %d", pObj->Id );
00719     printf( "\n" );
00720     printf( "POs: " );
00721     Ivy_ManForEachPo( p, pObj, i )
00722         printf( " %d", pObj->Id );
00723     printf( "\n" );
00724     printf( "Latches: " );
00725     Ivy_ManForEachLatch( p, pObj, i )
00726         printf( " %d=%d%s", pObj->Id, Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
00727     printf( "\n" );
00728     vNodes = Ivy_ManDfsSeq( p, NULL );
00729     Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
00730         Ivy_ObjPrintVerbose( p, pObj, fHaig ), printf( "\n" );
00731     printf( "\n" );
00732 }
00733 
00745 int Ivy_CutTruthPrint2( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth )
00746 {
00747     int i;
00748     printf( "Trying cut : {" );
00749     for ( i = 0; i < pCut->nSize; i++ )
00750         printf( " %6d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
00751     printf( " }   " );
00752     Extra_PrintBinary( stdout, &uTruth, 16 );  printf( "\n" );
00753     return 0;
00754 }
00755 
00767 int Ivy_CutTruthPrint( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth )
00768 {
00769     Vec_Ptr_t * vArray;
00770     Ivy_Obj_t * pObj, * pFanout;
00771     int nLatches = 0;
00772     int nPresent = 0;
00773     int i, k;
00774     int fVerbose = 0;
00775 
00776     if ( fVerbose )
00777         printf( "Trying cut : {" );
00778     for ( i = 0; i < pCut->nSize; i++ )
00779     {
00780         if ( fVerbose )
00781             printf( " %6d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
00782         nLatches += Ivy_LeafLat(pCut->pArray[i]);
00783     }
00784     if ( fVerbose )
00785         printf( " }   " );
00786     if ( fVerbose )
00787         printf( "Latches = %d. ", nLatches );
00788 
00789     // check if there are latches on the fanout edges
00790     vArray = Vec_PtrAlloc( 100 );
00791     for ( i = 0; i < pCut->nSize; i++ )
00792     {
00793         pObj = Ivy_ManObj( p, Ivy_LeafId(pCut->pArray[i]) );
00794         Ivy_ObjForEachFanout( p, pObj, vArray, pFanout, k )
00795         {
00796             if ( Ivy_ObjIsLatch(pFanout) )
00797             {
00798                 nPresent++;
00799                 break;
00800             }
00801         }
00802     }
00803     Vec_PtrSize( vArray );
00804     if ( fVerbose )
00805     {
00806         printf( "Present = %d. ", nPresent );
00807         if ( nLatches > nPresent )
00808             printf( "Clauses = %d. ", 2*(nLatches - nPresent) );
00809         printf( "\n" );
00810     }
00811     return ( nLatches > nPresent ) ? 2*(nLatches - nPresent) : 0;
00812 }
00813 
00817 
00818