00001
00021 #include "lpkInt.h"
00022 #include "cloud.h"
00023
00027
00031
00043 CloudNode * Lpk_CutTruthBdd_rec( CloudManager * dd, Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars )
00044 {
00045 CloudNode * pTruth, * pTruth0, * pTruth1;
00046 assert( !Hop_IsComplement(pObj) );
00047 if ( pObj->pData )
00048 {
00049 assert( ((unsigned)pObj->pData) & 0xffff0000 );
00050 return pObj->pData;
00051 }
00052
00053 if ( Hop_ObjIsConst1(pObj) )
00054 pTruth = dd->one;
00055 else
00056 {
00057 assert( Hop_ObjIsAnd(pObj) );
00058
00059 pTruth0 = Lpk_CutTruthBdd_rec( dd, pMan, Hop_ObjFanin0(pObj), nVars );
00060 pTruth1 = Lpk_CutTruthBdd_rec( dd, pMan, Hop_ObjFanin1(pObj), nVars );
00061 pTruth0 = Cloud_NotCond( pTruth0, Hop_ObjFaninC0(pObj) );
00062 pTruth1 = Cloud_NotCond( pTruth1, Hop_ObjFaninC1(pObj) );
00063
00064 pTruth = Cloud_bddAnd( dd, pTruth0, pTruth1 );
00065 }
00066 pObj->pData = pTruth;
00067 return pTruth;
00068 }
00069
00081 CloudNode * Lpk_CutTruthBdd( Lpk_Man_t * p, Lpk_Cut_t * pCut )
00082 {
00083 CloudManager * dd = p->pDsdMan->dd;
00084 Hop_Man_t * pManHop = p->pNtk->pManFunc;
00085 Hop_Obj_t * pObjHop;
00086 Abc_Obj_t * pObj, * pFanin;
00087 CloudNode * pTruth;
00088 int i, k, iCount = 0;
00089
00090
00091
00092
00093 Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
00094 pObj->pCopy = (Abc_Obj_t *)dd->vars[pCut->nLeaves-1-i];
00095
00096
00097 Lpk_CutForEachNodeReverse( p->pNtk, pCut, pObj, i )
00098 {
00099
00100 pObjHop = Hop_Regular(pObj->pData);
00101
00102 Hop_ObjCleanData_rec( pObjHop );
00103
00104 Abc_ObjForEachFanin( pObj, pFanin, k )
00105 {
00106 assert( ((unsigned)pFanin->pCopy) & 0xffff0000 );
00107 Hop_ManPi( pManHop, k )->pData = pFanin->pCopy;
00108 }
00109
00110 pTruth = Lpk_CutTruthBdd_rec( dd, pManHop, pObjHop, pCut->nLeaves );
00111 if ( Hop_IsComplement(pObj->pData) )
00112 pTruth = Cloud_Not(pTruth);
00113
00114 pObj->pCopy = (Abc_Obj_t *)pTruth;
00115
00116 }
00117
00118
00119
00120 return pTruth;
00121 }
00122
00123
00135 unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_Ptr_t * vTtNodes, int * piCount )
00136 {
00137 unsigned * pTruth, * pTruth0, * pTruth1;
00138 assert( !Hop_IsComplement(pObj) );
00139 if ( pObj->pData )
00140 {
00141 assert( ((unsigned)pObj->pData) & 0xffff0000 );
00142 return pObj->pData;
00143 }
00144
00145 pTruth = Vec_PtrEntry( vTtNodes, (*piCount)++ );
00146 if ( Hop_ObjIsConst1(pObj) )
00147 Kit_TruthFill( pTruth, nVars );
00148 else
00149 {
00150 assert( Hop_ObjIsAnd(pObj) );
00151
00152 pTruth0 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin0(pObj), nVars, vTtNodes, piCount );
00153 pTruth1 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin1(pObj), nVars, vTtNodes, piCount );
00154
00155 Kit_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Hop_ObjFaninC0(pObj), Hop_ObjFaninC1(pObj) );
00156 }
00157 pObj->pData = pTruth;
00158 return pTruth;
00159 }
00160
00172 unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fInv )
00173 {
00174 Hop_Man_t * pManHop = p->pNtk->pManFunc;
00175 Hop_Obj_t * pObjHop;
00176 Abc_Obj_t * pObj, * pFanin;
00177 unsigned * pTruth;
00178 int i, k, iCount = 0;
00179
00180 assert( pCut->nNodes > 0 );
00181
00182
00183 Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
00184 pObj->pCopy = Vec_PtrEntry( p->vTtElems, fInv? pCut->nLeaves-1-i : i );
00185
00186
00187 Lpk_CutForEachNodeReverse( p->pNtk, pCut, pObj, i )
00188 {
00189
00190 pObjHop = Hop_Regular(pObj->pData);
00191
00192 Hop_ObjCleanData_rec( pObjHop );
00193
00194 Abc_ObjForEachFanin( pObj, pFanin, k )
00195 {
00196 assert( ((unsigned)pFanin->pCopy) & 0xffff0000 );
00197 Hop_ManPi( pManHop, k )->pData = pFanin->pCopy;
00198 }
00199
00200 pTruth = Lpk_CutTruth_rec( pManHop, pObjHop, pCut->nLeaves, p->vTtNodes, &iCount );
00201 if ( Hop_IsComplement(pObj->pData) )
00202 Kit_TruthNot( pTruth, pTruth, pCut->nLeaves );
00203
00204 pObj->pCopy = (Abc_Obj_t *)pTruth;
00205 }
00206
00207
00208 if ( fInv == 0 )
00209 {
00210 pTruth = Vec_PtrEntry( p->vTtNodes, iCount++ );
00211 Kit_TruthCopy( pTruth, (unsigned *)pObj->pCopy, pCut->nLeaves );
00212 }
00213 assert( iCount <= Vec_PtrSize(p->vTtNodes) );
00214 return pTruth;
00215 }
00216
00217
00229 void Lpk_NodeRecordImpact( Lpk_Man_t * p )
00230 {
00231 Lpk_Cut_t * pCut;
00232 Vec_Ptr_t * vNodes = Vec_VecEntry( p->vVisited, p->pObj->Id );
00233 Abc_Obj_t * pNode;
00234 int i, k;
00235
00236 Vec_PtrClear( vNodes );
00237 for ( i = 0; i < p->nCuts; i++ )
00238 {
00239 pCut = p->pCuts + i;
00240 for ( k = 0; k < (int)pCut->nLeaves; k++ )
00241 {
00242 pNode = Abc_NtkObj( p->pNtk, pCut->pLeaves[k] );
00243 if ( pNode->fMarkC )
00244 continue;
00245 pNode->fMarkC = 1;
00246 Vec_PtrPush( vNodes, (void *)pNode->Id );
00247 Vec_PtrPush( vNodes, (void *)Abc_ObjFanoutNum(pNode) );
00248 }
00249 }
00250
00251 Vec_PtrForEachEntry( vNodes, pNode, i )
00252 {
00253 pNode = Abc_NtkObj( p->pNtk, (int)pNode );
00254 pNode->fMarkC = 0;
00255 i++;
00256 }
00257
00258 }
00259
00271 int Lpk_NodeCutsCheckDsd( Lpk_Man_t * p, Lpk_Cut_t * pCut )
00272 {
00273 Abc_Obj_t * pObj, * pFanin;
00274 int i, k, nCands, fLeavesOnly, RetValue;
00275 assert( pCut->nLeaves > 0 );
00276
00277 memset( p->pRefs, 0, sizeof(int) * pCut->nLeaves );
00278
00279 Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
00280 {
00281 assert( pObj->fMarkA == 0 );
00282 pObj->fMarkA = 1;
00283 pObj->pCopy = (void *)i;
00284 }
00285
00286 nCands = 0;
00287 Lpk_CutForEachNode( p->pNtk, pCut, pObj, i )
00288 {
00289 fLeavesOnly = 1;
00290 Abc_ObjForEachFanin( pObj, pFanin, k )
00291 if ( pFanin->fMarkA )
00292 p->pRefs[(int)pFanin->pCopy]++;
00293 else
00294 fLeavesOnly = 0;
00295 if ( fLeavesOnly )
00296 p->pCands[nCands++] = pObj->Id;
00297 }
00298
00299 RetValue = 0;
00300 for ( i = 0; i < nCands; i++ )
00301 {
00302 pObj = Abc_NtkObj( p->pNtk, p->pCands[i] );
00303 Abc_ObjForEachFanin( pObj, pFanin, k )
00304 {
00305 assert( pFanin->fMarkA == 1 );
00306 if ( p->pRefs[(int)pFanin->pCopy] > 1 )
00307 break;
00308 }
00309 if ( k == Abc_ObjFaninNum(pObj) )
00310 {
00311 RetValue = 1;
00312 break;
00313 }
00314 }
00315
00316 Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
00317 pObj->fMarkA = 0;
00318 return RetValue;
00319 }
00320
00332 static inline int Lpk_NodeCutsOneDominance( Lpk_Cut_t * pDom, Lpk_Cut_t * pCut )
00333 {
00334 int i, k;
00335 for ( i = 0; i < (int)pDom->nLeaves; i++ )
00336 {
00337 for ( k = 0; k < (int)pCut->nLeaves; k++ )
00338 if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
00339 break;
00340 if ( k == (int)pCut->nLeaves )
00341 return 0;
00342 }
00343
00344 return 1;
00345 }
00346
00358 int Lpk_NodeCutsOneFilter( Lpk_Cut_t * pCuts, int nCuts, Lpk_Cut_t * pCutNew )
00359 {
00360 Lpk_Cut_t * pCut;
00361 int i, k;
00362 assert( pCutNew->uSign[0] || pCutNew->uSign[1] );
00363
00364 for ( i = 0; i < nCuts; i++ )
00365 {
00366 pCut = pCuts + i;
00367 if ( pCut->nLeaves == 0 )
00368 continue;
00369 if ( pCut->nLeaves == pCutNew->nLeaves )
00370 {
00371 if ( pCut->uSign[0] == pCutNew->uSign[0] && pCut->uSign[1] == pCutNew->uSign[1] )
00372 {
00373 for ( k = 0; k < (int)pCutNew->nLeaves; k++ )
00374 if ( pCut->pLeaves[k] != pCutNew->pLeaves[k] )
00375 break;
00376 if ( k == (int)pCutNew->nLeaves )
00377 return 1;
00378 }
00379 continue;
00380 }
00381 if ( pCut->nLeaves < pCutNew->nLeaves )
00382 {
00383
00384 if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCut->uSign[0] )
00385 continue;
00386 if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCut->uSign[1] )
00387 continue;
00388
00389 if ( Lpk_NodeCutsOneDominance( pCut, pCutNew ) )
00390 return 1;
00391 continue;
00392 }
00393
00394
00395
00396 if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCutNew->uSign[0] )
00397 continue;
00398 if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCutNew->uSign[1] )
00399 continue;
00400
00401 if ( Lpk_NodeCutsOneDominance( pCutNew, pCut ) )
00402 pCut->nLeaves = 0;
00403 }
00404 return 0;
00405 }
00406
00418 void Lpk_NodePrintCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fLeavesOnly )
00419 {
00420 Abc_Obj_t * pObj;
00421 int i;
00422 if ( !fLeavesOnly )
00423 printf( "LEAVES:\n" );
00424 Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
00425 printf( "%d,", pObj->Id );
00426 if ( !fLeavesOnly )
00427 {
00428 printf( "\nNODES:\n" );
00429 Lpk_CutForEachNode( p->pNtk, pCut, pObj, i )
00430 {
00431 printf( "%d,", pObj->Id );
00432 assert( Abc_ObjIsNode(pObj) );
00433 }
00434 printf( "\n" );
00435 }
00436 }
00437
00449 void Lpk_NodeCutSignature( Lpk_Cut_t * pCut )
00450 {
00451 unsigned i;
00452 pCut->uSign[0] = pCut->uSign[1] = 0;
00453 for ( i = 0; i < pCut->nLeaves; i++ )
00454 {
00455 pCut->uSign[(pCut->pLeaves[i] & 32) > 0] |= (1 << (pCut->pLeaves[i] & 31));
00456 if ( i != pCut->nLeaves - 1 )
00457 assert( pCut->pLeaves[i] < pCut->pLeaves[i+1] );
00458 }
00459 }
00460
00461
00473 void Lpk_NodeCutsOne( Lpk_Man_t * p, Lpk_Cut_t * pCut, int Node )
00474 {
00475 Lpk_Cut_t * pCutNew;
00476 Abc_Obj_t * pObj, * pFanin;
00477 int i, k, j, nLeavesNew;
00478
00479
00480
00481
00482
00483
00484 if ( pCut->nNodes == LPK_SIZE_MAX )
00485 return;
00486
00487
00488 pObj = Abc_NtkObj( p->pNtk, Node );
00489 if ( Abc_ObjIsCi(pObj) )
00490 return;
00491 assert( Abc_ObjIsNode(pObj) );
00492 assert( Abc_ObjFaninNum(pObj) <= p->pPars->nLutSize );
00493
00494
00495 if ( !Abc_NodeIsTravIdCurrent(pObj) )
00496 {
00497 if ( (int)pCut->nNodesDup == p->pPars->nLutsOver )
00498 return;
00499 assert( (int)pCut->nNodesDup < p->pPars->nLutsOver );
00500 }
00501
00502
00503 nLeavesNew = pCut->nLeaves - 1;
00504 Abc_ObjForEachFanin( pObj, pFanin, i )
00505 {
00506 if ( (pCut->uSign[(pFanin->Id & 32) > 0] & (1 << (pFanin->Id & 31))) )
00507 continue;
00508 if ( ++nLeavesNew > p->pPars->nVarsMax )
00509 return;
00510 }
00511
00512
00513 assert( p->nCuts < LPK_CUTS_MAX );
00514 pCutNew = p->pCuts + p->nCuts;
00515 pCutNew->nLeaves = 0;
00516 for ( i = 0; i < (int)pCut->nLeaves; i++ )
00517 if ( pCut->pLeaves[i] != Node )
00518 pCutNew->pLeaves[pCutNew->nLeaves++] = pCut->pLeaves[i];
00519
00520
00521 Abc_ObjForEachFanin( pObj, pFanin, i )
00522 {
00523
00524 for ( k = 0; k < (int)pCutNew->nLeaves; k++ )
00525 if ( pCutNew->pLeaves[k] >= pFanin->Id )
00526 break;
00527 if ( k < (int)pCutNew->nLeaves && pCutNew->pLeaves[k] == pFanin->Id )
00528 continue;
00529
00530 if ( (int)pCutNew->nLeaves == p->pPars->nVarsMax )
00531 return;
00532
00533 for ( j = pCutNew->nLeaves; j > k; j-- )
00534 pCutNew->pLeaves[j] = pCutNew->pLeaves[j-1];
00535 pCutNew->pLeaves[k] = pFanin->Id;
00536 pCutNew->nLeaves++;
00537 assert( pCutNew->nLeaves <= LPK_SIZE_MAX );
00538
00539 }
00540
00541 Lpk_NodeCutSignature( pCutNew );
00542 if ( Lpk_NodeCutsOneFilter( p->pCuts, p->nCuts, pCutNew ) )
00543 return;
00544
00545
00546 assert( pCut->nNodes < LPK_SIZE_MAX );
00547 memcpy( pCutNew->pNodes, pCut->pNodes, pCut->nNodes * sizeof(int) );
00548 pCutNew->nNodes = pCut->nNodes;
00549 pCutNew->nNodesDup = pCut->nNodesDup;
00550
00551
00552
00553 for ( i = 0; i < (int)pCutNew->nNodes; i++ )
00554 if ( pCutNew->pNodes[i] == Node )
00555 {
00556 for ( k = i; k < (int)pCutNew->nNodes - 1; k++ )
00557 pCutNew->pNodes[k] = pCutNew->pNodes[k+1];
00558 pCutNew->pNodes[k] = Node;
00559 break;
00560 }
00561 if ( i == (int)pCutNew->nNodes )
00562 {
00563 pCutNew->pNodes[ pCutNew->nNodes++ ] = Node;
00564 pCutNew->nNodesDup += !Abc_NodeIsTravIdCurrent(pObj);
00565 }
00566
00567 assert( pCutNew->nNodes <= p->nMffc + pCutNew->nNodesDup );
00568
00569 assert( p->nCuts < LPK_CUTS_MAX );
00570 p->nCuts++;
00571 }
00572
00584 int Lpk_NodeCuts( Lpk_Man_t * p )
00585 {
00586 Lpk_Cut_t * pCut, * pCut2;
00587 int i, k, Temp, nMffc, fChanges;
00588
00589
00590 nMffc = p->nMffc = Abc_NodeMffcLabel( p->pObj );
00591 assert( nMffc > 0 );
00592 if ( nMffc == 1 )
00593 return 0;
00594
00595
00596 pCut = p->pCuts; p->nCuts = 1;
00597 pCut->nNodes = 0;
00598 pCut->nNodesDup = 0;
00599 pCut->nLeaves = 1;
00600 pCut->pLeaves[0] = p->pObj->Id;
00601
00602 Lpk_NodeCutSignature( pCut );
00603
00604
00605 for ( i = 0; i < p->nCuts; i++ )
00606 {
00607 pCut = p->pCuts + i;
00608 if ( pCut->nLeaves == 0 )
00609 continue;
00610
00611
00612 for ( k = 0; k < (int)pCut->nLeaves; k++ )
00613 {
00614
00615 Lpk_NodeCutsOne( p, pCut, pCut->pLeaves[k] );
00616
00617 if ( p->nCuts == LPK_CUTS_MAX )
00618 break;
00619 }
00620 if ( p->nCuts == LPK_CUTS_MAX )
00621 break;
00622 }
00623 if ( p->nCuts == LPK_CUTS_MAX )
00624 p->nNodesOver++;
00625
00626
00627 if ( p->pPars->fSatur )
00628 Lpk_NodeRecordImpact( p );
00629
00630
00631 p->nEvals = 0;
00632 for ( i = 0; i < p->nCuts; i++ )
00633 {
00634 pCut = p->pCuts + i;
00635 if ( pCut->nLeaves < 2 )
00636 continue;
00637
00638
00639 pCut->nLuts = Lpk_LutNumLuts( pCut->nLeaves, p->pPars->nLutSize );
00640
00641 pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts;
00642 if ( pCut->Weight <= 1.001 )
00643
00644 continue;
00645 pCut->fHasDsd = Lpk_NodeCutsCheckDsd( p, pCut );
00646 if ( pCut->fHasDsd )
00647 continue;
00648 p->pEvals[p->nEvals++] = i;
00649 }
00650 if ( p->nEvals == 0 )
00651 return 0;
00652
00653
00654 do {
00655 fChanges = 0;
00656 for ( i = 0; i < p->nEvals - 1; i++ )
00657 {
00658 pCut = p->pCuts + p->pEvals[i];
00659 pCut2 = p->pCuts + p->pEvals[i+1];
00660 if ( pCut->Weight >= pCut2->Weight - 0.001 )
00661 continue;
00662 Temp = p->pEvals[i];
00663 p->pEvals[i] = p->pEvals[i+1];
00664 p->pEvals[i+1] = Temp;
00665 fChanges = 1;
00666 }
00667 } while ( fChanges );
00668
00669
00670
00671
00672
00673
00674
00675
00676 return 1;
00677 }
00678
00682
00683