abc70930: src/aig/dar/darCut.c Source File

00001 
00021 #include "darInt.h"
00022 
00026 
00030 
00042 static inline int Dar_WordCountOnes( unsigned uWord )
00043 {
00044     uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
00045     uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
00046     uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
00047     uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
00048     return  (uWord & 0x0000FFFF) + (uWord>>16);
00049 }
00050 
00062 static inline int Dar_CutFindValue( Dar_Man_t * p, Dar_Cut_t * pCut )
00063 {
00064     Aig_Obj_t * pLeaf;
00065     int i, Value, nOnes;
00066     assert( pCut->fUsed );
00067     Value = 0;
00068     nOnes = 0;
00069     Dar_CutForEachLeaf( p->pAig, pCut, pLeaf, i )
00070     {
00071         if ( pLeaf == NULL )
00072             return 0;
00073         assert( pLeaf != NULL );
00074         Value += pLeaf->nRefs;
00075         nOnes += (pLeaf->nRefs == 1);
00076     }
00077     if ( pCut->nLeaves < 2 )
00078         return 1001;
00079 //    Value = Value * 100 / pCut->nLeaves;
00080     if ( Value > 1000 )
00081         Value = 1000;
00082     if ( nOnes > 3 )
00083         Value = 5 - nOnes;
00084     return Value;
00085 }
00086 
00098 static inline Dar_Cut_t * Dar_CutFindFree( Dar_Man_t * p, Aig_Obj_t * pObj )
00099 {
00100     Dar_Cut_t * pCut, * pCutMax;
00101     int i;
00102     pCutMax = NULL;
00103     Dar_ObjForEachCutAll( pObj, pCut, i )
00104     {
00105         if ( pCut->fUsed == 0 )
00106             return pCut;
00107         if ( pCut->nLeaves < 3 )
00108             continue;
00109         if ( pCutMax == NULL || pCutMax->Value > pCut->Value )
00110             pCutMax = pCut;
00111     }
00112     if ( pCutMax == NULL )
00113     {
00114         Dar_ObjForEachCutAll( pObj, pCut, i )
00115         {
00116             if ( pCut->nLeaves < 2 )
00117                 continue;
00118             if ( pCutMax == NULL || pCutMax->Value > pCut->Value )
00119                 pCutMax = pCut;
00120         }
00121     }
00122     if ( pCutMax == NULL )
00123     {
00124         Dar_ObjForEachCutAll( pObj, pCut, i )
00125         {
00126             if ( pCutMax == NULL || pCutMax->Value > pCut->Value )
00127                 pCutMax = pCut;
00128         }
00129     }
00130     assert( pCutMax != NULL );
00131     pCutMax->fUsed = 0;
00132     return pCutMax;
00133 }
00134 
00146 static inline int Dar_CutCheckDominance( Dar_Cut_t * pDom, Dar_Cut_t * pCut )
00147 {
00148     int i, k;
00149     assert( pDom->fUsed && pCut->fUsed );
00150     for ( i = 0; i < (int)pDom->nLeaves; i++ )
00151     {
00152         for ( k = 0; k < (int)pCut->nLeaves; k++ )
00153             if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
00154                 break;
00155         if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
00156             return 0;
00157     }
00158     // every node in pDom is contained in pCut
00159     return 1;
00160 }
00161 
00173 static inline int Dar_CutFilter( Aig_Obj_t * pObj, Dar_Cut_t * pCut )
00174 { 
00175     Dar_Cut_t * pTemp;
00176     int i;
00177     assert( pCut->fUsed );
00178     // go through the cuts of the node
00179     Dar_ObjForEachCut( pObj, pTemp, i )
00180     {
00181         if ( pTemp == pCut )
00182             continue;
00183         if ( pTemp->nLeaves > pCut->nLeaves )
00184         {
00185             // skip the non-contained cuts
00186             if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
00187                 continue;
00188             // check containment seriously
00189             if ( Dar_CutCheckDominance( pCut, pTemp ) )
00190             {
00191                 // remove contained cut
00192                 pTemp->fUsed = 0;
00193             }
00194          }
00195         else
00196         {
00197             // skip the non-contained cuts
00198             if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign )
00199                 continue;
00200             // check containment seriously
00201             if ( Dar_CutCheckDominance( pTemp, pCut ) )
00202             {
00203                 // remove the given cut
00204                 pCut->fUsed = 0;
00205                 return 1;
00206             }
00207         }
00208     }
00209     return 0;
00210 }
00211 
00223 static inline int Dar_CutMergeOrdered( Dar_Cut_t * pC, Dar_Cut_t * pC0, Dar_Cut_t * pC1 )
00224 { 
00225     int i, k, c;
00226     assert( pC0->nLeaves >= pC1->nLeaves );
00227 
00228     // the case of the largest cut sizes
00229     if ( pC0->nLeaves == 4 && pC1->nLeaves == 4 )
00230     {
00231         if ( pC0->uSign != pC1->uSign )
00232             return 0;
00233         for ( i = 0; i < (int)pC0->nLeaves; i++ )
00234             if ( pC0->pLeaves[i] != pC1->pLeaves[i] )
00235                 return 0;
00236         for ( i = 0; i < (int)pC0->nLeaves; i++ )
00237             pC->pLeaves[i] = pC0->pLeaves[i];
00238         pC->nLeaves = pC0->nLeaves;
00239         return 1;
00240     }
00241 
00242     // the case when one of the cuts is the largest
00243     if ( pC0->nLeaves == 4 )
00244     {
00245         if ( (pC0->uSign & pC1->uSign) != pC1->uSign )
00246             return 0;
00247         for ( i = 0; i < (int)pC1->nLeaves; i++ )
00248         {
00249             for ( k = (int)pC0->nLeaves - 1; k >= 0; k-- )
00250                 if ( pC0->pLeaves[k] == pC1->pLeaves[i] )
00251                     break;
00252             if ( k == -1 ) // did not find
00253                 return 0;
00254         }
00255         for ( i = 0; i < (int)pC0->nLeaves; i++ )
00256             pC->pLeaves[i] = pC0->pLeaves[i];
00257         pC->nLeaves = pC0->nLeaves;
00258         return 1;
00259     }
00260 
00261     // compare two cuts with different numbers
00262     i = k = 0;
00263     for ( c = 0; c < 4; c++ )
00264     {
00265         if ( k == (int)pC1->nLeaves )
00266         {
00267             if ( i == (int)pC0->nLeaves )
00268             {
00269                 pC->nLeaves = c;
00270                 return 1;
00271             }
00272             pC->pLeaves[c] = pC0->pLeaves[i++];
00273             continue;
00274         }
00275         if ( i == (int)pC0->nLeaves )
00276         {
00277             if ( k == (int)pC1->nLeaves )
00278             {
00279                 pC->nLeaves = c;
00280                 return 1;
00281             }
00282             pC->pLeaves[c] = pC1->pLeaves[k++];
00283             continue;
00284         }
00285         if ( pC0->pLeaves[i] < pC1->pLeaves[k] )
00286         {
00287             pC->pLeaves[c] = pC0->pLeaves[i++];
00288             continue;
00289         }
00290         if ( pC0->pLeaves[i] > pC1->pLeaves[k] )
00291         {
00292             pC->pLeaves[c] = pC1->pLeaves[k++];
00293             continue;
00294         }
00295         pC->pLeaves[c] = pC0->pLeaves[i++]; 
00296         k++;
00297     }
00298     if ( i < (int)pC0->nLeaves || k < (int)pC1->nLeaves )
00299         return 0;
00300     pC->nLeaves = c;
00301     return 1;
00302 }
00303 
00315 static inline int Dar_CutMerge( Dar_Cut_t * pCut, Dar_Cut_t * pCut0, Dar_Cut_t * pCut1 )
00316 { 
00317     assert( !pCut->fUsed );
00318     // merge the nodes
00319     if ( pCut0->nLeaves <= pCut1->nLeaves )
00320     {
00321         if ( !Dar_CutMergeOrdered( pCut, pCut1, pCut0 ) )
00322             return 0;
00323     }
00324     else
00325     {
00326         if ( !Dar_CutMergeOrdered( pCut, pCut0, pCut1 ) )
00327             return 0;
00328     }
00329     pCut->uSign = pCut0->uSign | pCut1->uSign;
00330     pCut->fUsed = 1;
00331     return 1;
00332 }
00333 
00334 
00346 static inline unsigned Dar_CutTruthPhase( Dar_Cut_t * pCut, Dar_Cut_t * pCut1 )
00347 {
00348     unsigned uPhase = 0;
00349     int i, k;
00350     for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
00351     {
00352         if ( k == (int)pCut1->nLeaves )
00353             break;
00354         if ( pCut->pLeaves[i] < pCut1->pLeaves[k] )
00355             continue;
00356         assert( pCut->pLeaves[i] == pCut1->pLeaves[k] );
00357         uPhase |= (1 << i);
00358         k++;
00359     }
00360     return uPhase;
00361 }
00362 
00374 static inline unsigned Dar_CutTruthSwapAdjacentVars( unsigned uTruth, int iVar )
00375 {
00376     assert( iVar >= 0 && iVar <= 2 );
00377     if ( iVar == 0 )
00378         return (uTruth & 0x99999999) | ((uTruth & 0x22222222) << 1) | ((uTruth & 0x44444444) >> 1);
00379     if ( iVar == 1 )
00380         return (uTruth & 0xC3C3C3C3) | ((uTruth & 0x0C0C0C0C) << 2) | ((uTruth & 0x30303030) >> 2);
00381     if ( iVar == 2 )
00382         return (uTruth & 0xF00FF00F) | ((uTruth & 0x00F000F0) << 4) | ((uTruth & 0x0F000F00) >> 4);
00383     assert( 0 );
00384     return 0;
00385 }
00386 
00400 static inline unsigned Dar_CutTruthStretch( unsigned uTruth, int nVars, unsigned Phase )
00401 {
00402     int i, k, Var = nVars - 1;
00403     for ( i = 3; i >= 0; i-- )
00404         if ( Phase & (1 << i) )
00405         {
00406             for ( k = Var; k < i; k++ )
00407                 uTruth = Dar_CutTruthSwapAdjacentVars( uTruth, k );
00408             Var--;
00409         }
00410     assert( Var == -1 );
00411     return uTruth;
00412 }
00413 
00427 static inline unsigned Dar_CutTruthShrink( unsigned uTruth, int nVars, unsigned Phase )
00428 {
00429     int i, k, Var = 0;
00430     for ( i = 0; i < 4; i++ )
00431         if ( Phase & (1 << i) )
00432         {
00433             for ( k = i-1; k >= Var; k-- )
00434                 uTruth = Dar_CutTruthSwapAdjacentVars( uTruth, k );
00435             Var++;
00436         }
00437     return uTruth;
00438 }
00439 
00451 static inline unsigned Dar_CutTruth( Dar_Cut_t * pCut, Dar_Cut_t * pCut0, Dar_Cut_t * pCut1, int fCompl0, int fCompl1 )
00452 {
00453     unsigned uTruth0 = fCompl0 ? ~pCut0->uTruth : pCut0->uTruth;
00454     unsigned uTruth1 = fCompl1 ? ~pCut1->uTruth : pCut1->uTruth;
00455     uTruth0 = Dar_CutTruthStretch( uTruth0, pCut0->nLeaves, Dar_CutTruthPhase(pCut, pCut0) );
00456     uTruth1 = Dar_CutTruthStretch( uTruth1, pCut1->nLeaves, Dar_CutTruthPhase(pCut, pCut1) );
00457     return uTruth0 & uTruth1;
00458 }
00459 
00471 static inline int Dar_CutSuppMinimize( Dar_Cut_t * pCut )
00472 {
00473     unsigned uMasks[4][2] = {
00474         { 0x5555, 0xAAAA },
00475         { 0x3333, 0xCCCC },
00476         { 0x0F0F, 0xF0F0 },
00477         { 0x00FF, 0xFF00 }
00478     };
00479     unsigned uPhase = 0, uTruth = 0xFFFF & pCut->uTruth;
00480     int i, k, nLeaves;
00481     assert( pCut->fUsed );
00482     // compute the truth support of the cut's function
00483     nLeaves = pCut->nLeaves;
00484     for ( i = 0; i < (int)pCut->nLeaves; i++ )
00485         if ( (uTruth & uMasks[i][0]) == ((uTruth & uMasks[i][1]) >> (1 << i)) )
00486             nLeaves--;
00487         else
00488             uPhase |= (1 << i);
00489     if ( nLeaves == (int)pCut->nLeaves )
00490         return 0;
00491     // shrink the truth table
00492     uTruth = Dar_CutTruthShrink( uTruth, pCut->nLeaves, uPhase );
00493     pCut->uTruth = 0xFFFF & uTruth;
00494     // update leaves and signature
00495     pCut->uSign = 0;
00496     for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
00497     {
00498         if ( !(uPhase & (1 << i)) )
00499             continue;    
00500         pCut->pLeaves[k++] = pCut->pLeaves[i];
00501         pCut->uSign |= Aig_ObjCutSign( pCut->pLeaves[i] );
00502     }
00503     assert( k == nLeaves );
00504     pCut->nLeaves = nLeaves;
00505     return 1;
00506 }
00507 
00519 void Dar_ManCutsFree( Dar_Man_t * p )
00520 {
00521     if ( p->pMemCuts == NULL )
00522         return;
00523     Aig_MmFixedStop( p->pMemCuts, 0 );
00524     p->pMemCuts = NULL;
00525 //    Aig_ManCleanData( p );
00526 }
00527 
00539 Dar_Cut_t * Dar_ObjPrepareCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
00540 {
00541     Dar_Cut_t * pCutSet, * pCut;
00542     int i;
00543     assert( Dar_ObjCuts(pObj) == NULL );
00544     pObj->nCuts = p->pPars->nCutsMax;
00545     // create the cutset of the node
00546     pCutSet = (Dar_Cut_t *)Aig_MmFixedEntryFetch( p->pMemCuts );
00547     Dar_ObjSetCuts( pObj, pCutSet );
00548     Dar_ObjForEachCut( pObj, pCut, i )
00549         pCut->fUsed = 0;
00550     // add unit cut if needed
00551     pCut = pCutSet;
00552     pCut->fUsed = 1;
00553     if ( Aig_ObjIsConst1(pObj) )
00554     {
00555         pCut->nLeaves = 0;
00556         pCut->uSign = 0;
00557         pCut->uTruth = 0xFFFF;
00558     }
00559     else
00560     {
00561         pCut->nLeaves = 1;
00562         pCut->pLeaves[0] = pObj->Id;
00563         pCut->uSign = Aig_ObjCutSign( pObj->Id );
00564         pCut->uTruth = 0xAAAA;
00565     }
00566     pCut->Value = Dar_CutFindValue( p, pCut );
00567     return pCutSet;
00568 }
00569 
00581 void Dar_ManCutsStart( Dar_Man_t * p )
00582 {
00583     Aig_Obj_t * pObj;
00584     int i;
00585     Aig_ManCleanData( p->pAig );
00586     Aig_MmFixedRestart( p->pMemCuts );
00587     Dar_ObjPrepareCuts( p, Aig_ManConst1(p->pAig) );
00588     Aig_ManForEachPi( p->pAig, pObj, i )
00589         Dar_ObjPrepareCuts( p, pObj );
00590 }
00591 
00603 Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
00604 {
00605     Aig_Obj_t * pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
00606     Aig_Obj_t * pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
00607     Aig_Obj_t * pFaninR0 = Aig_Regular(pFanin0);
00608     Aig_Obj_t * pFaninR1 = Aig_Regular(pFanin1);
00609     Dar_Cut_t * pCutSet, * pCut0, * pCut1, * pCut;
00610     int i, k, RetValue;
00611 
00612     assert( !Aig_IsComplement(pObj) );
00613     assert( Aig_ObjIsNode(pObj) );
00614     assert( Dar_ObjCuts(pObj) == NULL );
00615     assert( Dar_ObjCuts(pFaninR0) != NULL );
00616     assert( Dar_ObjCuts(pFaninR1) != NULL );
00617 
00618     // set up the first cut
00619     pCutSet = Dar_ObjPrepareCuts( p, pObj );
00620     // make sure fanins cuts are computed
00621     Dar_ObjForEachCut( pFaninR0, pCut0, i )
00622     Dar_ObjForEachCut( pFaninR1, pCut1, k )
00623     {
00624         p->nCutsAll++;
00625         // make sure K-feasible cut exists
00626         if ( Dar_WordCountOnes(pCut0->uSign | pCut1->uSign) > 4 )
00627             continue;
00628         // get the next cut of this node
00629         pCut = Dar_CutFindFree( p, pObj );
00630         // create the new cut
00631         if ( !Dar_CutMerge( pCut, pCut0, pCut1 ) )
00632         {
00633             assert( !pCut->fUsed );
00634             continue;
00635         }
00636         p->nCutsTried++;
00637         // check dominance
00638         if ( Dar_CutFilter( pObj, pCut ) )
00639         {
00640             assert( !pCut->fUsed );
00641             continue;
00642         }
00643         // compute truth table
00644         pCut->uTruth = 0xFFFF & Dar_CutTruth( pCut, pCut0, pCut1, Aig_IsComplement(pFanin0), Aig_IsComplement(pFanin1) );
00645 
00646         // minimize support of the cut
00647         if ( Dar_CutSuppMinimize( pCut ) )
00648         {
00649             RetValue = Dar_CutFilter( pObj, pCut );
00650             assert( !RetValue );
00651         }
00652 
00653         // assign the value of the cut
00654         pCut->Value = Dar_CutFindValue( p, pCut );
00655         // if the cut contains removed node, do not use it
00656         if ( pCut->Value == 0 )
00657         {
00658             p->nCutsSkipped++;
00659             pCut->fUsed = 0;
00660         }
00661         else if ( pCut->nLeaves < 2 )
00662             return pCutSet;
00663     }
00664     // count the number of nontrivial cuts cuts
00665     Dar_ObjForEachCut( pObj, pCut, i )
00666         p->nCutsUsed += pCut->fUsed;
00667     // discount trivial cut
00668     p->nCutsUsed--;
00669     return pCutSet;
00670 }
00671 
00683 Dar_Cut_t * Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj )
00684 {
00685     if ( Dar_ObjCuts(pObj) )
00686         return Dar_ObjCuts(pObj);
00687     if ( Aig_ObjIsBuf(pObj) )
00688         return Dar_ObjComputeCuts_rec( p, Aig_ObjFanin0(pObj) );
00689     Dar_ObjComputeCuts_rec( p, Aig_ObjFanin0(pObj) );
00690     Dar_ObjComputeCuts_rec( p, Aig_ObjFanin1(pObj) );
00691     return Dar_ObjComputeCuts( p, pObj );
00692 }
00693 
00697 
00698