src/aig/ivy/ivyCut.c File Reference

#include "ivy.h"
Include dependency graph for ivyCut.c:

Go to the source code of this file.

Functions

static int Ivy_NodeCutHashValue (int NodeId)
static int Ivy_NodeGetLeafCostOne (Ivy_Man_t *p, int Leaf, Vec_Int_t *vInside)
int Ivy_ManSeqFindCut_int (Ivy_Man_t *p, Vec_Int_t *vFront, Vec_Int_t *vInside, int nSizeLimit)
void Ivy_ManSeqFindCut (Ivy_Man_t *p, Ivy_Obj_t *pRoot, Vec_Int_t *vFront, Vec_Int_t *vInside, int nSize)
int Ivy_ManFindBoolCut_rec (Ivy_Man_t *p, Ivy_Obj_t *pObj, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vVolume, Ivy_Obj_t *pPivot)
int Ivy_ManFindBoolCutCost (Ivy_Obj_t *pObj)
int Ivy_ManFindBoolCut (Ivy_Man_t *p, Ivy_Obj_t *pRoot, Vec_Ptr_t *vFront, Vec_Ptr_t *vVolume, Vec_Ptr_t *vLeaves)
void Ivy_ManTestCutsBool (Ivy_Man_t *p)
static unsigned Ivy_NodeCutHash (Ivy_Cut_t *pCut)
static void Ivy_NodeCutShrink (Ivy_Cut_t *pCut, int iOld)
static int Ivy_NodeCutExtend (Ivy_Cut_t *pCut, int iNew)
static int Ivy_NodeCutPrescreen (Ivy_Cut_t *pCut, int Id0, int Id1)
static int Ivy_NodeCutDeriveNew (Ivy_Cut_t *pCut, Ivy_Cut_t *pCutNew, int IdOld, int IdNew0, int IdNew1)
int Ivy_NodeCutFindOrAdd (Ivy_Store_t *pCutStore, Ivy_Cut_t *pCutNew)
static int Ivy_CutCheckDominance (Ivy_Cut_t *pDom, Ivy_Cut_t *pCut)
int Ivy_NodeCutFindOrAddFilter (Ivy_Store_t *pCutStore, Ivy_Cut_t *pCutNew)
void Ivy_NodeCompactCuts (Ivy_Store_t *pCutStore)
void Ivy_NodePrintCut (Ivy_Cut_t *pCut)
void Ivy_NodePrintCuts (Ivy_Store_t *pCutStore)
static Ivy_Obj_t * Ivy_ObjRealFanin (Ivy_Obj_t *pObj)
Ivy_Store_t * Ivy_NodeFindCutsAll (Ivy_Man_t *p, Ivy_Obj_t *pObj, int nLeaves)
void Ivy_ManTestCutsAll (Ivy_Man_t *p)

Function Documentation

static int Ivy_CutCheckDominance ( Ivy_Cut_t *  pDom,
Ivy_Cut_t *  pCut 
) [inline, static]

Function*************************************************************

Synopsis [Returns 1 if pDom is contained in pCut.]

Description []

SideEffects []

SeeAlso []

Definition at line 712 of file ivyCut.c.

00713 {
00714     int i, k;
00715     for ( i = 0; i < pDom->nSize; i++ )
00716     {
00717         for ( k = 0; k < pCut->nSize; k++ )
00718             if ( pDom->pArray[i] == pCut->pArray[k] )
00719                 break;
00720         if ( k == pCut->nSize ) // node i in pDom is not contained in pCut
00721             return 0;
00722     }
00723     // every node in pDom is contained in pCut
00724     return 1;
00725 }

int Ivy_ManFindBoolCut ( Ivy_Man_t *  p,
Ivy_Obj_t *  pRoot,
Vec_Ptr_t *  vFront,
Vec_Ptr_t *  vVolume,
Vec_Ptr_t *  vLeaves 
)

Function*************************************************************

Synopsis [Computing Boolean cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 301 of file ivyCut.c.

00302 {
00303     Ivy_Obj_t * pObj, * pFaninC, * pFanin0, * pFanin1, * pPivot;
00304     int RetValue, LevelLimit, Lev, k;
00305     assert( !Ivy_IsComplement(pRoot) );
00306     // clear the frontier and collect the nodes
00307     Vec_PtrClear( vFront );
00308     Vec_PtrClear( vVolume );
00309     if ( Ivy_ObjIsMuxType(pRoot) )
00310         pFaninC = Ivy_ObjRecognizeMux( pRoot, &pFanin0, &pFanin1 );
00311     else
00312     {
00313         pFaninC = NULL;
00314         pFanin0 = Ivy_ObjFanin0(pRoot);
00315         pFanin1 = Ivy_ObjFanin1(pRoot); 
00316     }
00317     // start cone A
00318     pFanin0->fMarkA = 1;
00319     Vec_PtrPush( vFront, pFanin0 );
00320     Vec_PtrPush( vVolume, pFanin0 );
00321     // start cone B
00322     pFanin1->fMarkB = 1;
00323     Vec_PtrPush( vFront, pFanin1 );
00324     Vec_PtrPush( vVolume, pFanin1 );
00325     // iteratively expand until the common node (pPivot) is found or limit is reached
00326     assert( Ivy_ObjLevel(pRoot) == Ivy_ObjLevelNew(pRoot) );
00327     pPivot = NULL;
00328     LevelLimit = IVY_MAX( Ivy_ObjLevel(pRoot) - 10, 1 );
00329     for ( Lev = Ivy_ObjLevel(pRoot) - 1; Lev >= LevelLimit; Lev-- )
00330     {
00331         while ( 1 )
00332         {
00333             // find the next node to expand on this level
00334             Vec_PtrForEachEntry( vFront, pObj, k )
00335                 if ( (int)pObj->Level == Lev )
00336                     break;
00337             if ( k == Vec_PtrSize(vFront) )
00338                 break;
00339             assert( (int)pObj->Level <= Lev );
00340             assert( pObj->fMarkA ^ pObj->fMarkB );
00341             // remove the old node
00342             Vec_PtrRemove( vFront, pObj );
00343 
00344             // expand this node
00345             pFanin0 = Ivy_ObjFanin0(pObj);
00346             if ( !pFanin0->fMarkA && !pFanin0->fMarkB )
00347             {
00348                 Vec_PtrPush( vFront, pFanin0 );
00349                 Vec_PtrPush( vVolume, pFanin0 );
00350             }
00351             // mark the new nodes
00352             if ( pObj->fMarkA )
00353                 pFanin0->fMarkA = 1; 
00354             if ( pObj->fMarkB )
00355                 pFanin0->fMarkB = 1; 
00356 
00357             if ( Ivy_ObjIsBuf(pObj) )
00358             {
00359                 if ( pFanin0->fMarkA && pFanin0->fMarkB )
00360                 {
00361                     pPivot = pFanin0;
00362                     break;
00363                 }
00364                 continue;
00365             }
00366 
00367             // expand this node
00368             pFanin1 = Ivy_ObjFanin1(pObj); 
00369             if ( !pFanin1->fMarkA && !pFanin1->fMarkB )
00370             {
00371                 Vec_PtrPush( vFront, pFanin1 );
00372                 Vec_PtrPush( vVolume, pFanin1 );
00373             }
00374             // mark the new nodes
00375             if ( pObj->fMarkA )
00376                 pFanin1->fMarkA = 1; 
00377             if ( pObj->fMarkB )
00378                 pFanin1->fMarkB = 1; 
00379 
00380             // consider if it is time to quit
00381             if ( pFanin0->fMarkA && pFanin0->fMarkB )
00382             {
00383                 pPivot = pFanin0;
00384                 break;
00385             }
00386             if ( pFanin1->fMarkA && pFanin1->fMarkB )
00387             {
00388                 pPivot = pFanin1;
00389                 break;
00390             }
00391         }
00392         if ( pPivot != NULL )
00393             break;
00394     }
00395     if ( pPivot == NULL )
00396         return 0;
00397     // if the MUX control is defined, it should not be
00398     if ( pFaninC && !pFaninC->fMarkA && !pFaninC->fMarkB )
00399         Vec_PtrPush( vFront, pFaninC );
00400     // clean the markings
00401     Vec_PtrForEachEntry( vVolume, pObj, k )
00402         pObj->fMarkA = pObj->fMarkB = 0;
00403 
00404     // mark the nodes on the frontier (including the pivot)
00405     Vec_PtrForEachEntry( vFront, pObj, k )
00406         pObj->fMarkA = 1;
00407     // cut exists, collect all the nodes on the shortest path to the pivot
00408     Vec_PtrClear( vLeaves );
00409     Vec_PtrClear( vVolume );
00410     RetValue = Ivy_ManFindBoolCut_rec( p, pRoot, vLeaves, vVolume, pPivot );
00411     assert( RetValue == 1 );
00412     // unmark the nodes on the frontier (including the pivot)
00413     Vec_PtrForEachEntry( vFront, pObj, k )
00414         pObj->fMarkA = 0;
00415 
00416     // mark the nodes in the volume
00417     Vec_PtrForEachEntry( vVolume, pObj, k )
00418         pObj->fMarkA = 1;
00419     // expand the cut without increasing its size
00420     while ( 1 )
00421     {
00422         Vec_PtrForEachEntry( vLeaves, pObj, k )
00423             if ( Ivy_ManFindBoolCutCost(pObj) < 2 )
00424                 break;
00425         if ( k == Vec_PtrSize(vLeaves) )
00426             break;
00427         // the node can be expanded
00428         // remove the old node
00429         Vec_PtrRemove( vLeaves, pObj );
00430         // expand this node
00431         pFanin0 = Ivy_ObjFanin0(pObj);
00432         if ( !pFanin0->fMarkA )
00433         {
00434             pFanin0->fMarkA = 1;
00435             Vec_PtrPush( vVolume, pFanin0 );
00436             Vec_PtrPush( vLeaves, pFanin0 );
00437         }
00438         if ( Ivy_ObjIsBuf(pObj) )
00439             continue;
00440         // expand this node
00441         pFanin1 = Ivy_ObjFanin1(pObj);
00442         if ( !pFanin1->fMarkA )
00443         {
00444             pFanin1->fMarkA = 1;
00445             Vec_PtrPush( vVolume, pFanin1 );
00446             Vec_PtrPush( vLeaves, pFanin1 );
00447         }        
00448     }
00449     // unmark the nodes in the volume
00450     Vec_PtrForEachEntry( vVolume, pObj, k )
00451         pObj->fMarkA = 0;
00452     return 1;
00453 }

int Ivy_ManFindBoolCut_rec ( Ivy_Man_t *  p,
Ivy_Obj_t *  pObj,
Vec_Ptr_t *  vLeaves,
Vec_Ptr_t *  vVolume,
Ivy_Obj_t *  pPivot 
)

Function*************************************************************

Synopsis [Computing Boolean cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 218 of file ivyCut.c.

00219 {
00220     int RetValue0, RetValue1;
00221     if ( pObj == pPivot )
00222     {
00223         Vec_PtrPushUnique( vLeaves, pObj );
00224         Vec_PtrPushUnique( vVolume, pObj );
00225         return 1;        
00226     }
00227     if ( pObj->fMarkA )
00228         return 0;
00229 
00230 //    assert( !Ivy_ObjIsCi(pObj) );
00231     if ( Ivy_ObjIsCi(pObj) )
00232         return 0;
00233 
00234     if ( Ivy_ObjIsBuf(pObj) )
00235     {
00236         RetValue0 = Ivy_ManFindBoolCut_rec( p, Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot );
00237         if ( !RetValue0 )
00238             return 0;
00239         Vec_PtrPushUnique( vVolume, pObj );
00240         return 1;
00241     }
00242     assert( Ivy_ObjIsNode(pObj) );
00243     RetValue0 = Ivy_ManFindBoolCut_rec( p, Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot );
00244     RetValue1 = Ivy_ManFindBoolCut_rec( p, Ivy_ObjFanin1(pObj), vLeaves, vVolume, pPivot );
00245     if ( !RetValue0 && !RetValue1 )
00246         return 0;
00247     // add new leaves
00248     if ( !RetValue0 )
00249     {
00250         Vec_PtrPushUnique( vLeaves, Ivy_ObjFanin0(pObj) );
00251         Vec_PtrPushUnique( vVolume, Ivy_ObjFanin0(pObj) );
00252     }
00253     if ( !RetValue1 )
00254     {
00255         Vec_PtrPushUnique( vLeaves, Ivy_ObjFanin1(pObj) );
00256         Vec_PtrPushUnique( vVolume, Ivy_ObjFanin1(pObj) );
00257     }
00258     Vec_PtrPushUnique( vVolume, pObj );
00259     return 1;
00260 }

int Ivy_ManFindBoolCutCost ( Ivy_Obj_t *  pObj  ) 

Function*************************************************************

Synopsis [Returns the cost of one node (how many new nodes are added.]

Description []

SideEffects []

SeeAlso []

Definition at line 273 of file ivyCut.c.

00274 {
00275     int Cost;
00276     // make sure the node is in the construction zone
00277     assert( pObj->fMarkA == 1 );  
00278     // cannot expand over the PI node
00279     if ( Ivy_ObjIsCi(pObj) )
00280         return 999;
00281     // always expand over the buffer
00282     if ( Ivy_ObjIsBuf(pObj) )
00283         return !Ivy_ObjFanin0(pObj)->fMarkA;
00284     // get the cost of the cone
00285     Cost = (!Ivy_ObjFanin0(pObj)->fMarkA) + (!Ivy_ObjFanin1(pObj)->fMarkA);
00286     // return the number of nodes to be added to the leaves if this node is removed
00287     return Cost;
00288 }

void Ivy_ManSeqFindCut ( Ivy_Man_t *  p,
Ivy_Obj_t *  pRoot,
Vec_Int_t *  vFront,
Vec_Int_t *  vInside,
int  nSize 
)

Function*************************************************************

Synopsis [Computes one sequential cut of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 180 of file ivyCut.c.

00181 {
00182     assert( !Ivy_IsComplement(pRoot) );
00183     assert( Ivy_ObjIsNode(pRoot) );
00184     assert( Ivy_ObjFaninId0(pRoot) );
00185     assert( Ivy_ObjFaninId1(pRoot) );
00186 
00187     // start the cut 
00188     Vec_IntClear( vFront );
00189     Vec_IntPush( vFront, Ivy_LeafCreate(Ivy_ObjFaninId0(pRoot), 0) );
00190     Vec_IntPush( vFront, Ivy_LeafCreate(Ivy_ObjFaninId1(pRoot), 0) );
00191 
00192     // start the visited nodes
00193     Vec_IntClear( vInside );
00194     Vec_IntPush( vInside, Ivy_LeafCreate(pRoot->Id, 0) );
00195     Vec_IntPush( vInside, Ivy_LeafCreate(Ivy_ObjFaninId0(pRoot), 0) );
00196     Vec_IntPush( vInside, Ivy_LeafCreate(Ivy_ObjFaninId1(pRoot), 0) );
00197 
00198     // compute the cut
00199     while ( Ivy_ManSeqFindCut_int( p, vFront, vInside, nSize ) );
00200     assert( Vec_IntSize(vFront) <= nSize );
00201 }

int Ivy_ManSeqFindCut_int ( Ivy_Man_t *  p,
Vec_Int_t *  vFront,
Vec_Int_t *  vInside,
int  nSizeLimit 
)

Function*************************************************************

Synopsis [Builds reconvergence-driven cut by changing one leaf at a time.]

Description [This procedure looks at the current leaves and tries to change one leaf at a time in such a way that the cut grows as little as possible. In evaluating the fanins, this procedure looks only at their immediate predecessors (this is why it is called a one-level construction procedure).]

SideEffects []

SeeAlso []

Definition at line 87 of file ivyCut.c.

00088 {
00089     Ivy_Obj_t * pNode;
00090     int CostBest, CostCur, Leaf, LeafBest, Next, nLatches, i;
00091     int LeavesBest[10];
00092     int Counter;
00093 
00094     // add random selection of the best fanin!!!
00095 
00096     // find the best fanin
00097     CostBest = 99;
00098     LeafBest = -1;
00099     Counter = -1;
00100 //printf( "Evaluating fanins of the cut:\n" );
00101     Vec_IntForEachEntry( vFront, Leaf, i )
00102     {
00103         CostCur = Ivy_NodeGetLeafCostOne( p, Leaf, vInside );
00104 //printf( "    Fanin %s has cost %d.\n", Ivy_ObjName(pNode), CostCur );
00105         if ( CostBest > CostCur )
00106         {
00107             CostBest = CostCur;
00108             LeafBest = Leaf;
00109             LeavesBest[0] = Leaf;
00110             Counter = 1;
00111         }
00112         else if ( CostBest == CostCur )
00113             LeavesBest[Counter++] = Leaf;
00114 
00115         if ( CostBest <= 1 ) // can be if ( CostBest <= 1 )
00116             break;
00117     }
00118     if ( CostBest == 99 )
00119         return 0;
00120 //        return Ivy_NodeBuildCutLevelTwo_int( vInside, vFront, nFaninLimit );
00121 
00122     assert( CostBest < 3 );
00123     if ( Vec_IntSize(vFront) - 1 + CostBest > nSizeLimit )
00124         return 0;
00125 //        return Ivy_NodeBuildCutLevelTwo_int( vInside, vFront, nFaninLimit );
00126 
00127     assert( Counter > 0 );
00128 printf( "%d", Counter );
00129 
00130     LeafBest = LeavesBest[rand() % Counter];
00131 
00132     // remove the node from the array
00133     assert( LeafBest >= 0 );
00134     Vec_IntRemove( vFront, LeafBest );
00135 //printf( "Removing fanin %s.\n", Ivy_ObjName(pNode) );
00136 
00137     // get the node and its latches
00138     pNode = Ivy_ManObj( p, Ivy_LeafId(LeafBest) );
00139     nLatches = Ivy_LeafLat(LeafBest) + Ivy_ObjIsLatch(pNode);
00140     assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) );
00141 
00142     // add the left child to the fanins
00143     Next = Ivy_LeafCreate( Ivy_ObjFaninId0(pNode), nLatches );
00144     if ( Next && Vec_IntFind(vInside, Next) == -1 )
00145     {
00146 //printf( "Adding fanin %s.\n", Ivy_ObjName(pNext) );
00147         Vec_IntPush( vFront, Next );
00148         Vec_IntPush( vInside, Next );
00149     }
00150 
00151     // quit if this is the one fanin node
00152     if ( Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) )
00153         return 1;
00154     assert( Ivy_ObjIsNode(pNode) );
00155 
00156     // add the right child to the fanins
00157     Next = Ivy_LeafCreate( Ivy_ObjFaninId1(pNode), nLatches );
00158     if ( Next && Vec_IntFind(vInside, Next) == -1 )
00159     {
00160 //printf( "Adding fanin %s.\n", Ivy_ObjName(pNext) );
00161         Vec_IntPush( vFront, Next );
00162         Vec_IntPush( vInside, Next );
00163     }
00164     assert( Vec_IntSize(vFront) <= nSizeLimit );
00165     // keep doing this
00166     return 1;
00167 }

void Ivy_ManTestCutsAll ( Ivy_Man_t *  p  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 964 of file ivyCut.c.

00965 {
00966     Ivy_Obj_t * pObj;
00967     int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver;
00968     int clk = clock();
00969     nNodeTotal = nNodeOver = 0;
00970     nCutsTotal = -Ivy_ManNodeNum(p);
00971     Ivy_ManForEachObj( p, pObj, i )
00972     {
00973         if ( !Ivy_ObjIsNode(pObj) )
00974             continue;
00975         nCutsCut    = Ivy_NodeFindCutsAll( p, pObj, 5 )->nCuts;
00976         nCutsTotal += nCutsCut;
00977         nNodeOver  += (nCutsCut == IVY_CUT_LIMIT);
00978         nNodeTotal++;
00979     }
00980     printf( "Total cuts = %6d. Trivial = %6d.   Nodes = %6d. Satur = %6d.  ", 
00981         nCutsTotal, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
00982     PRT( "Time", clock() - clk );
00983 }

void Ivy_ManTestCutsBool ( Ivy_Man_t *  p  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 467 of file ivyCut.c.

00468 {
00469     Vec_Ptr_t * vFront, * vVolume, * vLeaves;
00470     Ivy_Obj_t * pObj;//, * pTemp;
00471     int i, RetValue;//, k;
00472     vFront = Vec_PtrAlloc( 100 );
00473     vVolume = Vec_PtrAlloc( 100 );
00474     vLeaves = Vec_PtrAlloc( 100 );
00475     Ivy_ManForEachObj( p, pObj, i )
00476     {
00477         if ( !Ivy_ObjIsNode(pObj) )
00478             continue;
00479         if ( Ivy_ObjIsMuxType(pObj) )
00480         {
00481             printf( "m" );
00482             continue;
00483         }
00484         if ( Ivy_ObjIsExor(pObj) )
00485             printf( "x" );
00486         RetValue = Ivy_ManFindBoolCut( p, pObj, vFront, vVolume, vLeaves );
00487         if ( RetValue == 0 )
00488             printf( "- " );
00489         else
00490             printf( "%d ", Vec_PtrSize(vLeaves) );
00491 /*        
00492         printf( "( " );
00493         Vec_PtrForEachEntry( vFront, pTemp, k )
00494             printf( "%d ", Ivy_ObjRefs(Ivy_Regular(pTemp)) );
00495         printf( ")\n" );
00496 */
00497     }
00498     printf( "\n" );
00499     Vec_PtrFree( vFront );
00500     Vec_PtrFree( vVolume );
00501     Vec_PtrFree( vLeaves );
00502 }

void Ivy_NodeCompactCuts ( Ivy_Store_t *  pCutStore  ) 

Function*************************************************************

Synopsis [Print the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 805 of file ivyCut.c.

00806 {
00807     Ivy_Cut_t * pCut;
00808     int i, k;
00809     for ( i = k = 0; i < pCutStore->nCuts; i++ )
00810     {
00811         pCut = pCutStore->pCuts + i;
00812         if ( pCut->nSize == 0 )
00813             continue;
00814         pCutStore->pCuts[k++] = *pCut;
00815     }
00816     pCutStore->nCuts = k;
00817 }

static int Ivy_NodeCutDeriveNew ( Ivy_Cut_t *  pCut,
Ivy_Cut_t *  pCutNew,
int  IdOld,
int  IdNew0,
int  IdNew1 
) [inline, static]

Function*************************************************************

Synopsis [Derives new cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 616 of file ivyCut.c.

00617 {
00618     unsigned uHash = 0;
00619     int i, k; 
00620     assert( pCut->nSize > 0 );
00621     assert( IdNew0 < IdNew1 );
00622     for ( i = k = 0; i < pCut->nSize; i++ )
00623     {
00624         if ( pCut->pArray[i] == IdOld )
00625             continue;
00626         if ( IdNew0 <= pCut->pArray[i] )
00627         {
00628             if ( IdNew0 < pCut->pArray[i] )
00629             {
00630                 pCutNew->pArray[ k++ ] = IdNew0;
00631                 uHash |= Ivy_NodeCutHashValue( IdNew0 );
00632             }
00633             IdNew0 = 0x7FFFFFFF;
00634         }
00635         if ( IdNew1 <= pCut->pArray[i] )
00636         {
00637             if ( IdNew1 < pCut->pArray[i] )
00638             {
00639                 pCutNew->pArray[ k++ ] = IdNew1;
00640                 uHash |= Ivy_NodeCutHashValue( IdNew1 );
00641             }
00642             IdNew1 = 0x7FFFFFFF;
00643         }
00644         pCutNew->pArray[ k++ ] = pCut->pArray[i];
00645         uHash |= Ivy_NodeCutHashValue( pCut->pArray[i] );
00646     }
00647     if ( IdNew0 < 0x7FFFFFFF )
00648     {
00649         pCutNew->pArray[ k++ ] = IdNew0;
00650         uHash |= Ivy_NodeCutHashValue( IdNew0 );
00651     }
00652     if ( IdNew1 < 0x7FFFFFFF )
00653     {
00654         pCutNew->pArray[ k++ ] = IdNew1;
00655         uHash |= Ivy_NodeCutHashValue( IdNew1 );
00656     }
00657     pCutNew->nSize = k;
00658     pCutNew->uHash = uHash;
00659     assert( pCutNew->nSize <= pCut->nSizeMax );
00660 //    for ( i = 1; i < pCutNew->nSize; i++ )
00661 //        assert( pCutNew->pArray[i-1] < pCutNew->pArray[i] );
00662     return 1;
00663 }

static int Ivy_NodeCutExtend ( Ivy_Cut_t *  pCut,
int  iNew 
) [inline, static]

Function*************************************************************

Synopsis [Adds one node to the cut.]

Description [Returns 1 if the cuts is still okay.]

SideEffects []

SeeAlso []

Definition at line 560 of file ivyCut.c.

00561 {
00562     int i;
00563     for ( i = 0; i < pCut->nSize; i++ )
00564         if ( pCut->pArray[i] == iNew )
00565             return 1;
00566     // check if there is room
00567     if ( pCut->nSize == pCut->nSizeMax )
00568         return 0;
00569     // add the new one
00570     for ( i = pCut->nSize - 1; i >= 0; i-- )
00571         if ( pCut->pArray[i] > iNew )
00572             pCut->pArray[i+1] = pCut->pArray[i];
00573         else
00574         {
00575             assert( pCut->pArray[i] < iNew );
00576             break;
00577         }
00578     pCut->pArray[i+1] = iNew;
00579     pCut->nSize++;
00580     return 1;
00581 }

int Ivy_NodeCutFindOrAdd ( Ivy_Store_t *  pCutStore,
Ivy_Cut_t *  pCutNew 
)

Function*************************************************************

Synopsis [Check if the cut exists.]

Description [Returns 1 if the cut exists.]

SideEffects []

SeeAlso []

Definition at line 676 of file ivyCut.c.

00677 {
00678     Ivy_Cut_t * pCut;
00679     int i, k;
00680     assert( pCutNew->uHash );
00681     // try to find the cut
00682     for ( i = 0; i < pCutStore->nCuts; i++ )
00683     {
00684         pCut = pCutStore->pCuts + i;
00685         if ( pCut->uHash == pCutNew->uHash && pCut->nSize == pCutNew->nSize )
00686         {
00687             for ( k = 0; k < pCutNew->nSize; k++ )
00688                 if ( pCut->pArray[k] != pCutNew->pArray[k] )
00689                     break;
00690             if ( k == pCutNew->nSize )
00691                 return 1;
00692         }
00693     }
00694     assert( pCutStore->nCuts < pCutStore->nCutsMax );
00695     // add the cut
00696     pCut = pCutStore->pCuts + pCutStore->nCuts++;
00697     *pCut = *pCutNew;
00698     return 0;
00699 }

int Ivy_NodeCutFindOrAddFilter ( Ivy_Store_t *  pCutStore,
Ivy_Cut_t *  pCutNew 
)

Function*************************************************************

Synopsis [Check if the cut exists.]

Description [Returns 1 if the cut exists.]

SideEffects []

SeeAlso []

Definition at line 738 of file ivyCut.c.

00739 {
00740     Ivy_Cut_t * pCut;
00741     int i, k;
00742     assert( pCutNew->uHash );
00743     // try to find the cut
00744     for ( i = 0; i < pCutStore->nCuts; i++ )
00745     {
00746         pCut = pCutStore->pCuts + i;
00747         if ( pCut->nSize == 0 )
00748             continue;
00749         if ( pCut->nSize == pCutNew->nSize )
00750         {
00751             if ( pCut->uHash == pCutNew->uHash )
00752             {
00753                 for ( k = 0; k < pCutNew->nSize; k++ )
00754                     if ( pCut->pArray[k] != pCutNew->pArray[k] )
00755                         break;
00756                 if ( k == pCutNew->nSize )
00757                     return 1;
00758             }
00759             continue;
00760         }
00761         if ( pCut->nSize < pCutNew->nSize )
00762         {
00763             // skip the non-contained cuts
00764             if ( (pCut->uHash & pCutNew->uHash) != pCut->uHash )
00765                 continue;
00766             // check containment seriously
00767             if ( Ivy_CutCheckDominance( pCut, pCutNew ) )
00768                 return 1;
00769             continue;
00770         }
00771         // check potential containment of other cut
00772 
00773         // skip the non-contained cuts
00774         if ( (pCut->uHash & pCutNew->uHash) != pCutNew->uHash )
00775             continue;
00776         // check containment seriously
00777         if ( Ivy_CutCheckDominance( pCutNew, pCut ) )
00778         {
00779             // remove the current cut
00780 //            --pCutStore->nCuts;
00781 //            for ( k = i; k < pCutStore->nCuts; k++ )
00782 //                pCutStore->pCuts[k] = pCutStore->pCuts[k+1];
00783 //            i--;
00784             pCut->nSize = 0;
00785         }
00786     }
00787     assert( pCutStore->nCuts < pCutStore->nCutsMax );
00788     // add the cut
00789     pCut = pCutStore->pCuts + pCutStore->nCuts++;
00790     *pCut = *pCutNew;
00791     return 0;
00792 }

static unsigned Ivy_NodeCutHash ( Ivy_Cut_t *  pCut  )  [inline, static]

Function*************************************************************

Synopsis [Find the hash value of the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 517 of file ivyCut.c.

00518 {
00519     int i;
00520 //    for ( i = 1; i < pCut->nSize; i++ )
00521 //        assert( pCut->pArray[i-1] < pCut->pArray[i] );
00522     pCut->uHash = 0;
00523     for ( i = 0; i < pCut->nSize; i++ )
00524         pCut->uHash |= (1 << (pCut->pArray[i] % 31));
00525     return pCut->uHash;
00526 }

static int Ivy_NodeCutHashValue ( int  NodeId  )  [inline, static]

CFile****************************************************************

FileName [ivyCut.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis [Computes reconvergence driven sequential cut.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id
ivyCut.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

] DECLARATIONS ///

Definition at line 27 of file ivyCut.c.

00027 { return 1 << (NodeId % 31); }

static int Ivy_NodeCutPrescreen ( Ivy_Cut_t *  pCut,
int  Id0,
int  Id1 
) [inline, static]

Function*************************************************************

Synopsis [Returns 1 if the cut can be constructed; 0 otherwise.]

Description []

SideEffects []

SeeAlso []

Definition at line 594 of file ivyCut.c.

00595 {
00596     int i;
00597     if ( pCut->nSize < pCut->nSizeMax )
00598         return 1;
00599     for ( i = 0; i < pCut->nSize; i++ )
00600         if ( pCut->pArray[i] == Id0 || pCut->pArray[i] == Id1 )
00601             return 1;
00602     return 0;
00603 }

static void Ivy_NodeCutShrink ( Ivy_Cut_t *  pCut,
int  iOld 
) [inline, static]

Function*************************************************************

Synopsis [Removes one node to the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 539 of file ivyCut.c.

00540 {
00541     int i, k;
00542     for ( i = k = 0; i < pCut->nSize; i++ )
00543         if ( pCut->pArray[i] != iOld )
00544             pCut->pArray[k++] = pCut->pArray[i];
00545     assert( k == pCut->nSize - 1 );
00546     pCut->nSize--;
00547 }

Ivy_Store_t* Ivy_NodeFindCutsAll ( Ivy_Man_t *  p,
Ivy_Obj_t *  pObj,
int  nLeaves 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 888 of file ivyCut.c.

00889 {
00890     static Ivy_Store_t CutStore, * pCutStore = &CutStore;
00891     Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut;
00892     Ivy_Obj_t * pLeaf;
00893     int i, k, iLeaf0, iLeaf1;
00894 
00895     assert( nLeaves <= IVY_CUT_INPUT );
00896 
00897     // start the structure
00898     pCutStore->nCuts = 0;
00899     pCutStore->nCutsMax = IVY_CUT_LIMIT;
00900     // start the trivial cut
00901     pCutNew->uHash = 0;
00902     pCutNew->nSize = 1;
00903     pCutNew->nSizeMax = nLeaves;
00904     pCutNew->pArray[0] = pObj->Id;
00905     Ivy_NodeCutHash( pCutNew );
00906     // add the trivial cut
00907     Ivy_NodeCutFindOrAdd( pCutStore, pCutNew );
00908     assert( pCutStore->nCuts == 1 );
00909 
00910     // explore the cuts
00911     for ( i = 0; i < pCutStore->nCuts; i++ )
00912     {
00913         // expand this cut
00914         pCut = pCutStore->pCuts + i;
00915         if ( pCut->nSize == 0 )
00916             continue;
00917         for ( k = 0; k < pCut->nSize; k++ )
00918         {
00919             pLeaf = Ivy_ManObj( p, pCut->pArray[k] );
00920             if ( Ivy_ObjIsCi(pLeaf) )
00921                 continue;
00922 /*
00923             *pCutNew = *pCut;
00924             Ivy_NodeCutShrink( pCutNew, pLeaf->Id );
00925             if ( !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId0(pLeaf) ) )
00926                 continue;
00927             if ( Ivy_ObjIsNode(pLeaf) && !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId1(pLeaf) ) )
00928                 continue;
00929             Ivy_NodeCutHash( pCutNew );
00930 */
00931             iLeaf0 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin0(pLeaf)) );
00932             iLeaf1 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin1(pLeaf)) );
00933 //            if ( iLeaf0 == iLeaf1 ) // strange situation observed on Jan 18, 2007
00934 //                continue;
00935             if ( !Ivy_NodeCutPrescreen( pCut, iLeaf0, iLeaf1 ) )
00936                 continue;
00937             if ( iLeaf0 > iLeaf1 )
00938                 Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf1, iLeaf0 );
00939             else
00940                 Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf0, iLeaf1 );
00941             Ivy_NodeCutFindOrAddFilter( pCutStore, pCutNew );
00942             if ( pCutStore->nCuts == IVY_CUT_LIMIT )
00943                 break;
00944         }
00945         if ( pCutStore->nCuts == IVY_CUT_LIMIT )
00946             break;
00947     }
00948     Ivy_NodeCompactCuts( pCutStore );
00949 //    Ivy_NodePrintCuts( pCutStore );
00950     return pCutStore;
00951 }

static int Ivy_NodeGetLeafCostOne ( Ivy_Man_t *  p,
int  Leaf,
Vec_Int_t *  vInside 
) [inline, static]

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Evaluate the cost of removing the node from the set of leaves.]

Description [Returns the number of new leaves that will be brought in. Returns large number if the node cannot be removed from the set of leaves.]

SideEffects []

SeeAlso []

Definition at line 45 of file ivyCut.c.

00046 {
00047     Ivy_Obj_t * pNode;
00048     int nLatches, FaninLeaf, Cost;
00049     // make sure leaf is not a contant node
00050     assert( Leaf > 0 ); 
00051     // get the node
00052     pNode = Ivy_ManObj( p, Ivy_LeafId(Leaf) );
00053     // cannot expand over the PI node
00054     if ( Ivy_ObjIsPi(pNode) || Ivy_ObjIsConst1(pNode) )
00055         return 999;
00056     // get the number of latches
00057     nLatches = Ivy_LeafLat(Leaf) + Ivy_ObjIsLatch(pNode);
00058     if ( nLatches > 15 )
00059         return 999;
00060     // get the first fanin
00061     FaninLeaf = Ivy_LeafCreate( Ivy_ObjFaninId0(pNode), nLatches );
00062     Cost = FaninLeaf && (Vec_IntFind(vInside, FaninLeaf) == -1);
00063     // quit if this is the one fanin node
00064     if ( Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) )
00065         return Cost;
00066     assert( Ivy_ObjIsNode(pNode) );
00067     // get the second fanin
00068     FaninLeaf = Ivy_LeafCreate( Ivy_ObjFaninId1(pNode), nLatches );
00069     Cost += FaninLeaf && (Vec_IntFind(vInside, FaninLeaf) == -1);
00070     return Cost;
00071 }

void Ivy_NodePrintCut ( Ivy_Cut_t *  pCut  ) 

Function*************************************************************

Synopsis [Print the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 830 of file ivyCut.c.

00831 {
00832     int i;
00833     assert( pCut->nSize > 0 );
00834     printf( "%d : {", pCut->nSize );
00835     for ( i = 0; i < pCut->nSize; i++ )
00836         printf( " %d", pCut->pArray[i] );
00837     printf( " }\n" );
00838 }

void Ivy_NodePrintCuts ( Ivy_Store_t *  pCutStore  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 851 of file ivyCut.c.

00852 {
00853     int i;
00854     printf( "Node %d\n", pCutStore->pCuts[0].pArray[0] );
00855     for ( i = 0; i < pCutStore->nCuts; i++ )
00856         Ivy_NodePrintCut( pCutStore->pCuts + i );
00857 }

static Ivy_Obj_t* Ivy_ObjRealFanin ( Ivy_Obj_t *  pObj  )  [inline, static]

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 870 of file ivyCut.c.

00871 {
00872     if ( !Ivy_ObjIsBuf(pObj) )
00873         return pObj;
00874     return Ivy_ObjRealFanin( Ivy_ObjFanin0(pObj) );
00875 }

Generated on Tue Jan 5 12:18:23 2010 for abc70930 by  doxygen 1.6.1