ivyCutTrav.c File Reference

#include "ivy.h"

Go to the source code of this file.

Functions
static ABC_NAMESPACE_IMPL_START unsigned *	Ivy_NodeCutElementary (Vec_Int_t *vStore, int nWords, int NodeId)
	DECLARATIONS ///. More...
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)
	FUNCTION DEFINITIONS ///. More...
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  )

inlinestatic

Definition at line 363 of file ivyCutTrav.c.

{
    int w;
    for ( w = nWords-1; w >= 0; w-- )
        if ( pIn1[w] & ~pIn2[w] )
            return 0;
    return 1;
}

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

inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 357 of file ivyCutTrav.c.

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

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

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

Synopsis [Compares the node by level.]

Description []

SideEffects []

SeeAlso []

Definition at line 161 of file ivyCutTrav.c.

{
    Ivy_Obj_t * pObj1 = *ppObj1;
    Ivy_Obj_t * pObj2 = *ppObj2;
    if ( pObj1->Level < pObj2->Level )
        return -1;
    if ( pObj1->Level > pObj2->Level )
        return 1;
    return 0;
}

void Ivy_ManTestCutsTravAll

(

Ivy_Man_t *

p

)

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

Synopsis [Compute the set of all cuts.]

Description []

SideEffects []

SeeAlso []

Definition at line 434 of file ivyCutTrav.c.

{
    Ivy_Store_t * pStore;
    Ivy_Obj_t * pObj;
    Vec_Ptr_t * vNodes, * vFront;
    Vec_Int_t * vStore;
    Vec_Vec_t * vBitCuts;
    int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver;
    abctime clk = Abc_Clock();

    vNodes = Vec_PtrAlloc( 100 );
    vFront = Vec_PtrAlloc( 100 );
    vStore = Vec_IntAlloc( 100 );
    vBitCuts = Vec_VecAlloc( 100 );

    nNodeTotal = nNodeOver = 0;
    nCutsTotal = -Ivy_ManNodeNum(p);
    Ivy_ManForEachObj( p, pObj, i )
    {
        if ( !Ivy_ObjIsNode(pObj) )
            continue;
        pStore = Ivy_NodeFindCutsTravAll( p, pObj, 4, 60, vNodes, vFront, vStore, vBitCuts );
        nCutsCut    = pStore->nCuts;
        nCutsTotal += nCutsCut;
        nNodeOver  += (nCutsCut == IVY_CUT_LIMIT);
        nNodeTotal++;
    }
    printf( "Total cuts = %6d. Trivial = %6d.   Nodes = %6d. Satur = %6d.  ", 
        nCutsTotal, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
    ABC_PRT( "Time", Abc_Clock() - clk );

    Vec_PtrFree( vNodes );
    Vec_PtrFree( vFront );
    Vec_IntFree( vStore );
    Vec_VecFree( vBitCuts );

}

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 223 of file ivyCutTrav.c.

{
    Ivy_Obj_t * pTemp, * pFanin;
    int i, nNodes;
    // mark nodes up to the given depth
    Ivy_NodeComputeVolumeTrav1_rec( pObj, 6 );
    // collect the marked nodes
    Vec_PtrClear( vFront );
    Ivy_NodeComputeVolumeTrav2_rec( pObj, vFront );
    // find the fanins that are not marked
    Vec_PtrClear( vNodes );
    Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pTemp, i )
    {
        pFanin = Ivy_ObjFanin0(pTemp);
        if ( !pFanin->fMarkA )
        {
            pFanin->fMarkA = 1;
            Vec_PtrPush( vNodes, pFanin );
        }
        pFanin = Ivy_ObjFanin1(pTemp);
        if ( !pFanin->fMarkA )
        {
            pFanin->fMarkA = 1;
            Vec_PtrPush( vNodes, pFanin );
        }
    }
    // remember the number of nodes in the frontier
    nNodes = Vec_PtrSize( vNodes );
    // add the remaining nodes
    Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pTemp, i )
        Vec_PtrPush( vNodes, pTemp );
    // unmark the nodes
    Vec_PtrForEachEntry( Ivy_Obj_t *, vNodes, pTemp, i )
    {
        pTemp->fMarkA = 0;
        pTemp->TravId = i;
    }
    // collect the frontier nodes
    Vec_PtrClear( vFront );
    Vec_PtrForEachEntryStop( Ivy_Obj_t *, vNodes, pTemp, i, nNodes )
        Vec_PtrPush( vFront, pTemp );
//    printf( "%d ", Vec_PtrSize(vNodes) );
}

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 278 of file ivyCutTrav.c.

{
    Ivy_Obj_t * pLeaf, * pPivot, * pFanin;
    int LevelMax, i;
    assert( Ivy_ObjIsNode(pObj) );
    // clear arrays
    Vec_PtrClear( vNodes );
    Vec_PtrClear( vFront );
    // add the root
    pObj->fMarkA = 1;
    Vec_PtrPush( vNodes, pObj );
    Vec_PtrPush( vFront, pObj );
    // expand node with maximum level
    LevelMax = pObj->Level;
    do {
        // get the node to expand
        pPivot = NULL;
        Vec_PtrForEachEntryReverse( Ivy_Obj_t *, vFront, pLeaf, i )
        {
            if ( (int)pLeaf->Level == LevelMax )
            {
                pPivot = pLeaf;
                break;
            }
        }
        // decrease level if we did not find the node
        if ( pPivot == NULL )
        {
            if ( --LevelMax == 0 )
                break;
            continue;
        }
        // the node to expand is found
        // remove it from frontier
        Vec_PtrRemove( vFront, pPivot );
        // add fanins
        pFanin = Ivy_ObjFanin0(pPivot); 
        if ( !pFanin->fMarkA )
        {
            pFanin->fMarkA = 1;
            Vec_PtrPush( vNodes, pFanin );
            Vec_PtrPush( vFront, pFanin );
        }
        pFanin = Ivy_ObjFanin1(pPivot); 
        if ( pFanin && !pFanin->fMarkA )
        {
            pFanin->fMarkA = 1;
            Vec_PtrPush( vNodes, pFanin );
            Vec_PtrPush( vFront, pFanin );
        }
        // quit if we collected enough nodes
    } while ( Vec_PtrSize(vNodes) < nNodeLimit );

    // sort nodes by level
    Vec_PtrSort( vNodes, (int (*)(void))Ivy_CompareNodesByLevel );
    // make sure the nodes are ordered in the increasing number of levels
    pFanin = (Ivy_Obj_t *)Vec_PtrEntry( vNodes, 0 );
    pPivot = (Ivy_Obj_t *)Vec_PtrEntryLast( vNodes );
    assert( pFanin->Level <= pPivot->Level );

    // clean the marks and remember node numbers in the TravId
    Vec_PtrForEachEntry( Ivy_Obj_t *, vNodes, pFanin, i )
    {
        pFanin->fMarkA = 0;
        pFanin->TravId = i;
    }
}

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 183 of file ivyCutTrav.c.

{
    if ( Ivy_ObjIsCi(pObj) || Depth == 0 )
        return;
    Ivy_NodeComputeVolumeTrav1_rec( Ivy_ObjFanin0(pObj), Depth - 1 );
    Ivy_NodeComputeVolumeTrav1_rec( Ivy_ObjFanin1(pObj), Depth - 1 );
    pObj->fMarkA = 1;
}

void Ivy_NodeComputeVolumeTrav2_rec	(	Ivy_Obj_t *	pObj,
		Vec_Ptr_t *	vNodes
	)

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

Synopsis [Collect the marked nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 203 of file ivyCutTrav.c.

{
    if ( !pObj->fMarkA )
        return;
    Ivy_NodeComputeVolumeTrav2_rec( Ivy_ObjFanin0(pObj), vNodes );
    Ivy_NodeComputeVolumeTrav2_rec( Ivy_ObjFanin1(pObj), vNodes );
    Vec_PtrPush( vNodes, pObj );
}

unsigned * Ivy_NodeCutElementary ( Vec_Int_t *  vStore, int  nWords, int  NodeId  )

static

DECLARATIONS ///.

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

]

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

Synopsis [Creates elementary bit-cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 141 of file ivyCutTrav.c.

{
    unsigned * pBitCut;
    pBitCut = Vec_IntFetch( vStore, nWords );
    memset( pBitCut, 0, 4 * nWords );
    Extra_TruthSetBit( pBitCut, NodeId );
    return pBitCut;
}

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 383 of file ivyCutTrav.c.

{
    unsigned * pBitCut, * pBitCut0, * pBitCut1, * pBitCutTest;
    int i, k, c, w, Counter;
    // iterate through the cut pairs
    Vec_PtrForEachEntry( unsigned *, vCuts0, pBitCut0, i )
    Vec_PtrForEachEntry( unsigned *, vCuts1, pBitCut1, k )
    {
        // skip infeasible cuts
        Counter = 0;
        for ( w = 0; w < nWords; w++ )
        {
            Counter += Extra_WordCountOnes( pBitCut0[w] | pBitCut1[w] );
            if ( Counter > nLeaves )
                break;
        }
        if ( Counter > nLeaves )
            continue;
        // the new cut is feasible - create it
        pBitCutTest = Vec_IntFetch( vStore, nWords );
        Extra_TruthOrWords( pBitCutTest, pBitCut0, pBitCut1, nWords );
        // filter contained cuts; try to find containing cut
        w = 0;
        Vec_PtrForEachEntry( unsigned *, vCuts, pBitCut, c )
        {
            if ( Extra_TruthIsImplyWords( pBitCut, pBitCutTest, nWords ) )
                break;
            if ( Extra_TruthIsImplyWords( pBitCutTest, pBitCut, nWords ) )
                continue;
            Vec_PtrWriteEntry( vCuts, w++, pBitCut );
        }
        if ( c != Vec_PtrSize(vCuts) )
            continue;
        Vec_PtrShrink( vCuts, w );
        // add the cut
        Vec_PtrPush( vCuts, pBitCutTest );
    }
}

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 49 of file ivyCutTrav.c.

{
    static Ivy_Store_t CutStore, * pCutStore = &CutStore;
    Vec_Ptr_t * vCuts, * vCuts0, * vCuts1;
    unsigned * pBitCut;
    Ivy_Obj_t * pLeaf;
    Ivy_Cut_t * pCut;
    int i, k, nWords, nNodes;

    assert( nLeaves <= IVY_CUT_INPUT );

    // find the given number of nodes in the TFI
    Ivy_NodeComputeVolume( pObj, nNodeLimit - 1, vNodes, vFront );
    nNodes = Vec_PtrSize(vNodes);
//    assert( nNodes <= nNodeLimit );

    // make sure vBitCuts has enough room
    Vec_VecExpand( vBitCuts, nNodes-1 );
    Vec_VecClear( vBitCuts );

    // prepare the memory manager
    Vec_IntClear( vStore );
    Vec_IntGrow( vStore, 64000 );

    // set elementary cuts for the leaves
    nWords = Extra_BitWordNum( nNodes );
    Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pLeaf, i )
    {
        assert( Ivy_ObjTravId(pLeaf) < nNodes );
        // get the new bitcut
        pBitCut = Ivy_NodeCutElementary( vStore, nWords, Ivy_ObjTravId(pLeaf) );
        // set it as the cut of this leaf
        Vec_VecPush( vBitCuts, Ivy_ObjTravId(pLeaf), pBitCut );
    }

    // compute the cuts for each node
    Vec_PtrForEachEntry( Ivy_Obj_t *, vNodes, pLeaf, i )
    {
        // skip the leaves
        vCuts = Vec_VecEntry( vBitCuts, Ivy_ObjTravId(pLeaf) );
        if ( Vec_PtrSize(vCuts) > 0 )
            continue;
        // add elementary cut
        pBitCut = Ivy_NodeCutElementary( vStore, nWords, Ivy_ObjTravId(pLeaf) );
        // set it as the cut of this leaf
        Vec_VecPush( vBitCuts, Ivy_ObjTravId(pLeaf), pBitCut );
        // get the fanin cuts
        vCuts0 = Vec_VecEntry( vBitCuts, Ivy_ObjTravId( Ivy_ObjFanin0(pLeaf) ) );
        vCuts1 = Vec_VecEntry( vBitCuts, Ivy_ObjTravId( Ivy_ObjFanin1(pLeaf) ) );
        assert( Vec_PtrSize(vCuts0) > 0 );
        assert( Vec_PtrSize(vCuts1) > 0 );
        // merge the cuts
        Ivy_NodeFindCutsMerge( vCuts0, vCuts1, vCuts, nLeaves, nWords, vStore );
    }

    // start the structure
    pCutStore->nCuts = 0;
    pCutStore->nCutsMax = IVY_CUT_LIMIT;
    // collect the cuts of the root node
    vCuts = Vec_VecEntry( vBitCuts, Ivy_ObjTravId(pObj) );
    Vec_PtrForEachEntry( unsigned *, vCuts, pBitCut, i )
    {
        pCut = pCutStore->pCuts + pCutStore->nCuts++;
        pCut->nSize = 0;
        pCut->nSizeMax = nLeaves;
        pCut->uHash = 0;
        for ( k = 0; k < nNodes; k++ )
            if ( Extra_TruthHasBit(pBitCut, k) )
                pCut->pArray[ pCut->nSize++ ] = Ivy_ObjId( (Ivy_Obj_t *)Vec_PtrEntry(vNodes, k) );
        assert( pCut->nSize <= nLeaves );
        if ( pCutStore->nCuts == pCutStore->nCutsMax )
            break;
    }

    // clean the travIds
    Vec_PtrForEachEntry( Ivy_Obj_t *, vNodes, pLeaf, i )
        pLeaf->TravId = 0;
    return pCutStore;
}