src/aig/ivy/ivyCutTrav.c File Reference

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

Go to the source code of this file.

Functions

static unsigned * Ivy_NodeCutElementary (Vec_Int_t *vStore, int nWords, int NodeId)
static void Ivy_NodeComputeVolume (Ivy_Obj_t *pObj, int nNodeLimit, Vec_Ptr_t *vNodes, Vec_Ptr_t *vFront)
static void Ivy_NodeFindCutsMerge (Vec_Ptr_t *vCuts0, Vec_Ptr_t *vCuts1, Vec_Ptr_t *vCuts, int nLeaves, int nWords, Vec_Int_t *vStore)
Ivy_Store_t * Ivy_NodeFindCutsTravAll (Ivy_Man_t *p, Ivy_Obj_t *pObj, int nLeaves, int nNodeLimit, Vec_Ptr_t *vNodes, Vec_Ptr_t *vFront, Vec_Int_t *vStore, Vec_Vec_t *vBitCuts)
int Ivy_CompareNodesByLevel (Ivy_Obj_t **ppObj1, Ivy_Obj_t **ppObj2)
void Ivy_NodeComputeVolumeTrav1_rec (Ivy_Obj_t *pObj, int Depth)
void Ivy_NodeComputeVolumeTrav2_rec (Ivy_Obj_t *pObj, Vec_Ptr_t *vNodes)
void Ivy_NodeComputeVolume2 (Ivy_Obj_t *pObj, int nNodeLimit, Vec_Ptr_t *vNodes, Vec_Ptr_t *vFront)
static void Extra_TruthOrWords (unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nWords)
static int Extra_TruthIsImplyWords (unsigned *pIn1, unsigned *pIn2, int nWords)
void Ivy_ManTestCutsTravAll (Ivy_Man_t *p)

Function Documentation

static int Extra_TruthIsImplyWords ( unsigned *  pIn1,
unsigned *  pIn2,
int  nWords 
) [inline, static]

Definition at line 360 of file ivyCutTrav.c.

00361 {
00362     int w;
00363     for ( w = nWords-1; w >= 0; w-- )
00364         if ( pIn1[w] & ~pIn2[w] )
00365             return 0;
00366     return 1;
00367 }

static void Extra_TruthOrWords ( unsigned *  pOut,
unsigned *  pIn0,
unsigned *  pIn1,
int  nWords 
) [inline, static]

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 354 of file ivyCutTrav.c.

00355 {
00356     int w;
00357     for ( w = nWords-1; w >= 0; w-- )
00358         pOut[w] = pIn0[w] | pIn1[w];
00359 }

int Ivy_CompareNodesByLevel ( Ivy_Obj_t **  ppObj1,
Ivy_Obj_t **  ppObj2 
)

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

Synopsis [Compares the node by level.]

Description []

SideEffects []

SeeAlso []

Definition at line 158 of file ivyCutTrav.c.

00159 {
00160     Ivy_Obj_t * pObj1 = *ppObj1;
00161     Ivy_Obj_t * pObj2 = *ppObj2;
00162     if ( pObj1->Level < pObj2->Level )
00163         return -1;
00164     if ( pObj1->Level > pObj2->Level )
00165         return 1;
00166     return 0;
00167 }

void Ivy_ManTestCutsTravAll ( Ivy_Man_t *  p  ) 

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

Synopsis [Compute the set of all cuts.]

Description []

SideEffects []

SeeAlso []

Definition at line 431 of file ivyCutTrav.c.

00432 {
00433     Ivy_Store_t * pStore;
00434     Ivy_Obj_t * pObj;
00435     Vec_Ptr_t * vNodes, * vFront;
00436     Vec_Int_t * vStore;
00437     Vec_Vec_t * vBitCuts;
00438     int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver;
00439     int clk = clock();
00440 
00441     vNodes = Vec_PtrAlloc( 100 );
00442     vFront = Vec_PtrAlloc( 100 );
00443     vStore = Vec_IntAlloc( 100 );
00444     vBitCuts = Vec_VecAlloc( 100 );
00445 
00446     nNodeTotal = nNodeOver = 0;
00447     nCutsTotal = -Ivy_ManNodeNum(p);
00448     Ivy_ManForEachObj( p, pObj, i )
00449     {
00450         if ( !Ivy_ObjIsNode(pObj) )
00451             continue;
00452         pStore = Ivy_NodeFindCutsTravAll( p, pObj, 4, 60, vNodes, vFront, vStore, vBitCuts );
00453         nCutsCut    = pStore->nCuts;
00454         nCutsTotal += nCutsCut;
00455         nNodeOver  += (nCutsCut == IVY_CUT_LIMIT);
00456         nNodeTotal++;
00457     }
00458     printf( "Total cuts = %6d. Trivial = %6d.   Nodes = %6d. Satur = %6d.  ", 
00459         nCutsTotal, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
00460     PRT( "Time", clock() - clk );
00461 
00462     Vec_PtrFree( vNodes );
00463     Vec_PtrFree( vFront );
00464     Vec_IntFree( vStore );
00465     Vec_VecFree( vBitCuts );
00466 
00467 }

void Ivy_NodeComputeVolume ( Ivy_Obj_t *  pObj,
int  nNodeLimit,
Vec_Ptr_t *  vNodes,
Vec_Ptr_t *  vFront 
) [static]

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 220 of file ivyCutTrav.c.

00221 {
00222     Ivy_Obj_t * pTemp, * pFanin;
00223     int i, nNodes;
00224     // mark nodes up to the given depth
00225     Ivy_NodeComputeVolumeTrav1_rec( pObj, 6 );
00226     // collect the marked nodes
00227     Vec_PtrClear( vFront );
00228     Ivy_NodeComputeVolumeTrav2_rec( pObj, vFront );
00229     // find the fanins that are not marked
00230     Vec_PtrClear( vNodes );
00231     Vec_PtrForEachEntry( vFront, pTemp, i )
00232     {
00233         pFanin = Ivy_ObjFanin0(pTemp);
00234         if ( !pFanin->fMarkA )
00235         {
00236             pFanin->fMarkA = 1;
00237             Vec_PtrPush( vNodes, pFanin );
00238         }
00239         pFanin = Ivy_ObjFanin1(pTemp);
00240         if ( !pFanin->fMarkA )
00241         {
00242             pFanin->fMarkA = 1;
00243             Vec_PtrPush( vNodes, pFanin );
00244         }
00245     }
00246     // remember the number of nodes in the frontier
00247     nNodes = Vec_PtrSize( vNodes );
00248     // add the remaining nodes
00249     Vec_PtrForEachEntry( vFront, pTemp, i )
00250         Vec_PtrPush( vNodes, pTemp );
00251     // unmark the nodes
00252     Vec_PtrForEachEntry( vNodes, pTemp, i )
00253     {
00254         pTemp->fMarkA = 0;
00255         pTemp->TravId = i;
00256     }
00257     // collect the frontier nodes
00258     Vec_PtrClear( vFront );
00259     Vec_PtrForEachEntryStop( vNodes, pTemp, i, nNodes )
00260         Vec_PtrPush( vFront, pTemp );
00261 //    printf( "%d ", Vec_PtrSize(vNodes) );
00262 }

void Ivy_NodeComputeVolume2 ( Ivy_Obj_t *  pObj,
int  nNodeLimit,
Vec_Ptr_t *  vNodes,
Vec_Ptr_t *  vFront 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 275 of file ivyCutTrav.c.

00276 {
00277     Ivy_Obj_t * pLeaf, * pPivot, * pFanin;
00278     int LevelMax, i;
00279     assert( Ivy_ObjIsNode(pObj) );
00280     // clear arrays
00281     Vec_PtrClear( vNodes );
00282     Vec_PtrClear( vFront );
00283     // add the root
00284     pObj->fMarkA = 1;
00285     Vec_PtrPush( vNodes, pObj );
00286     Vec_PtrPush( vFront, pObj );
00287     // expand node with maximum level
00288     LevelMax = pObj->Level;
00289     do {
00290         // get the node to expand
00291         pPivot = NULL;
00292         Vec_PtrForEachEntryReverse( vFront, pLeaf, i )
00293         {
00294             if ( (int)pLeaf->Level == LevelMax )
00295             {
00296                 pPivot = pLeaf;
00297                 break;
00298             }
00299         }
00300         // decrease level if we did not find the node
00301         if ( pPivot == NULL )
00302         {
00303             if ( --LevelMax == 0 )
00304                 break;
00305             continue;
00306         }
00307         // the node to expand is found
00308         // remove it from frontier
00309         Vec_PtrRemove( vFront, pPivot );
00310         // add fanins
00311         pFanin = Ivy_ObjFanin0(pPivot); 
00312         if ( !pFanin->fMarkA )
00313         {
00314             pFanin->fMarkA = 1;
00315             Vec_PtrPush( vNodes, pFanin );
00316             Vec_PtrPush( vFront, pFanin );
00317         }
00318         pFanin = Ivy_ObjFanin1(pPivot); 
00319         if ( pFanin && !pFanin->fMarkA )
00320         {
00321             pFanin->fMarkA = 1;
00322             Vec_PtrPush( vNodes, pFanin );
00323             Vec_PtrPush( vFront, pFanin );
00324         }
00325         // quit if we collected enough nodes
00326     } while ( Vec_PtrSize(vNodes) < nNodeLimit );
00327 
00328     // sort nodes by level
00329     Vec_PtrSort( vNodes, Ivy_CompareNodesByLevel );
00330     // make sure the nodes are ordered in the increasing number of levels
00331     pFanin = Vec_PtrEntry( vNodes, 0 );
00332     pPivot = Vec_PtrEntryLast( vNodes );
00333     assert( pFanin->Level <= pPivot->Level );
00334 
00335     // clean the marks and remember node numbers in the TravId
00336     Vec_PtrForEachEntry( vNodes, pFanin, i )
00337     {
00338         pFanin->fMarkA = 0;
00339         pFanin->TravId = i;
00340     }
00341 }

void Ivy_NodeComputeVolumeTrav1_rec ( Ivy_Obj_t *  pObj,
int  Depth 
)

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

Synopsis [Mark all nodes up to the given depth.]

Description []

SideEffects []

SeeAlso []

Definition at line 180 of file ivyCutTrav.c.

00181 {
00182     if ( Ivy_ObjIsCi(pObj) || Depth == 0 )
00183         return;
00184     Ivy_NodeComputeVolumeTrav1_rec( Ivy_ObjFanin0(pObj), Depth - 1 );
00185     Ivy_NodeComputeVolumeTrav1_rec( Ivy_ObjFanin1(pObj), Depth - 1 );
00186     pObj->fMarkA = 1;
00187 }

void Ivy_NodeComputeVolumeTrav2_rec ( Ivy_Obj_t *  pObj,
Vec_Ptr_t *  vNodes 
)

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

Synopsis [Collect the marked nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 200 of file ivyCutTrav.c.

00201 {
00202     if ( !pObj->fMarkA )
00203         return;
00204     Ivy_NodeComputeVolumeTrav2_rec( Ivy_ObjFanin0(pObj), vNodes );
00205     Ivy_NodeComputeVolumeTrav2_rec( Ivy_ObjFanin1(pObj), vNodes );
00206     Vec_PtrPush( vNodes, pObj );
00207 }

unsigned * Ivy_NodeCutElementary ( Vec_Int_t *  vStore,
int  nWords,
int  NodeId 
) [static]

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

FileName [ivyCutTrav.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

] DECLARATIONS ///

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

Synopsis [Creates elementary bit-cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 138 of file ivyCutTrav.c.

00139 {
00140     unsigned * pBitCut;
00141     pBitCut = Vec_IntFetch( vStore, nWords );
00142     memset( pBitCut, 0, 4 * nWords );
00143     Extra_TruthSetBit( pBitCut, NodeId );
00144     return pBitCut;
00145 }

void Ivy_NodeFindCutsMerge ( Vec_Ptr_t *  vCuts0,
Vec_Ptr_t *  vCuts1,
Vec_Ptr_t *  vCuts,
int  nLeaves,
int  nWords,
Vec_Int_t *  vStore 
) [static]

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

Synopsis [Merges two sets of bit-cuts at a node.]

Description []

SideEffects []

SeeAlso []

Definition at line 380 of file ivyCutTrav.c.

00382 {
00383     unsigned * pBitCut, * pBitCut0, * pBitCut1, * pBitCutTest;
00384     int i, k, c, w, Counter;
00385     // iterate through the cut pairs
00386     Vec_PtrForEachEntry( vCuts0, pBitCut0, i )
00387     Vec_PtrForEachEntry( vCuts1, pBitCut1, k )
00388     {
00389         // skip infeasible cuts
00390         Counter = 0;
00391         for ( w = 0; w < nWords; w++ )
00392         {
00393             Counter += Extra_WordCountOnes( pBitCut0[w] | pBitCut1[w] );
00394             if ( Counter > nLeaves )
00395                 break;
00396         }
00397         if ( Counter > nLeaves )
00398             continue;
00399         // the new cut is feasible - create it
00400         pBitCutTest = Vec_IntFetch( vStore, nWords );
00401         Extra_TruthOrWords( pBitCutTest, pBitCut0, pBitCut1, nWords );
00402         // filter contained cuts; try to find containing cut
00403         w = 0;
00404         Vec_PtrForEachEntry( vCuts, pBitCut, c )
00405         {
00406             if ( Extra_TruthIsImplyWords( pBitCut, pBitCutTest, nWords ) )
00407                 break;
00408             if ( Extra_TruthIsImplyWords( pBitCutTest, pBitCut, nWords ) )
00409                 continue;
00410             Vec_PtrWriteEntry( vCuts, w++, pBitCut );
00411         }
00412         if ( c != Vec_PtrSize(vCuts) )
00413             continue;
00414         Vec_PtrShrink( vCuts, w );
00415         // add the cut
00416         Vec_PtrPush( vCuts, pBitCutTest );
00417     }
00418 }

Ivy_Store_t* Ivy_NodeFindCutsTravAll ( Ivy_Man_t *  p,
Ivy_Obj_t *  pObj,
int  nLeaves,
int  nNodeLimit,
Vec_Ptr_t *  vNodes,
Vec_Ptr_t *  vFront,
Vec_Int_t *  vStore,
Vec_Vec_t *  vBitCuts 
)

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

Synopsis [Computes cuts for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file ivyCutTrav.c.

00048 {
00049     static Ivy_Store_t CutStore, * pCutStore = &CutStore;
00050     Vec_Ptr_t * vCuts, * vCuts0, * vCuts1;
00051     unsigned * pBitCut;
00052     Ivy_Obj_t * pLeaf;
00053     Ivy_Cut_t * pCut;
00054     int i, k, nWords, nNodes;
00055 
00056     assert( nLeaves <= IVY_CUT_INPUT );
00057 
00058     // find the given number of nodes in the TFI
00059     Ivy_NodeComputeVolume( pObj, nNodeLimit - 1, vNodes, vFront );
00060     nNodes = Vec_PtrSize(vNodes);
00061 //    assert( nNodes <= nNodeLimit );
00062 
00063     // make sure vBitCuts has enough room
00064     Vec_VecExpand( vBitCuts, nNodes-1 );
00065     Vec_VecClear( vBitCuts );
00066 
00067     // prepare the memory manager
00068     Vec_IntClear( vStore );
00069     Vec_IntGrow( vStore, 64000 );
00070 
00071     // set elementary cuts for the leaves
00072     nWords = Extra_BitWordNum( nNodes );
00073     Vec_PtrForEachEntry( vFront, pLeaf, i )
00074     {
00075         assert( Ivy_ObjTravId(pLeaf) < nNodes );
00076         // get the new bitcut
00077         pBitCut = Ivy_NodeCutElementary( vStore, nWords, Ivy_ObjTravId(pLeaf) );
00078         // set it as the cut of this leaf
00079         Vec_VecPush( vBitCuts, Ivy_ObjTravId(pLeaf), pBitCut );
00080     }
00081 
00082     // compute the cuts for each node
00083     Vec_PtrForEachEntry( vNodes, pLeaf, i )
00084     {
00085         // skip the leaves
00086         vCuts = Vec_VecEntry( vBitCuts, Ivy_ObjTravId(pLeaf) );
00087         if ( Vec_PtrSize(vCuts) > 0 )
00088             continue;
00089         // add elementary cut
00090         pBitCut = Ivy_NodeCutElementary( vStore, nWords, Ivy_ObjTravId(pLeaf) );
00091         // set it as the cut of this leaf
00092         Vec_VecPush( vBitCuts, Ivy_ObjTravId(pLeaf), pBitCut );
00093         // get the fanin cuts
00094         vCuts0 = Vec_VecEntry( vBitCuts, Ivy_ObjTravId( Ivy_ObjFanin0(pLeaf) ) );
00095         vCuts1 = Vec_VecEntry( vBitCuts, Ivy_ObjTravId( Ivy_ObjFanin1(pLeaf) ) );
00096         assert( Vec_PtrSize(vCuts0) > 0 );
00097         assert( Vec_PtrSize(vCuts1) > 0 );
00098         // merge the cuts
00099         Ivy_NodeFindCutsMerge( vCuts0, vCuts1, vCuts, nLeaves, nWords, vStore );
00100     }
00101 
00102     // start the structure
00103     pCutStore->nCuts = 0;
00104     pCutStore->nCutsMax = IVY_CUT_LIMIT;
00105     // collect the cuts of the root node
00106     vCuts = Vec_VecEntry( vBitCuts, Ivy_ObjTravId(pObj) );
00107     Vec_PtrForEachEntry( vCuts, pBitCut, i )
00108     {
00109         pCut = pCutStore->pCuts + pCutStore->nCuts++;
00110         pCut->nSize = 0;
00111         pCut->nSizeMax = nLeaves;
00112         pCut->uHash = 0;
00113         for ( k = 0; k < nNodes; k++ )
00114             if ( Extra_TruthHasBit(pBitCut, k) )
00115                 pCut->pArray[ pCut->nSize++ ] = Ivy_ObjId( Vec_PtrEntry(vNodes, k) );
00116         assert( pCut->nSize <= nLeaves );
00117         if ( pCutStore->nCuts == pCutStore->nCutsMax )
00118             break;
00119     }
00120 
00121     // clean the travIds
00122     Vec_PtrForEachEntry( vNodes, pLeaf, i )
00123         pLeaf->TravId = 0;
00124     return pCutStore;
00125 }

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