ivyBalance.c File Reference

#include "ivy.h"

Go to the source code of this file.

Functions
static ABC_NAMESPACE_IMPL_START int	Ivy_NodeBalance_rec (Ivy_Man_t *pNew, Ivy_Obj_t *pObj, Vec_Vec_t *vStore, int Level, int fUpdateLevel)
	DECLARATIONS ///. More...
static Vec_Ptr_t *	Ivy_NodeBalanceCone (Ivy_Obj_t *pObj, Vec_Vec_t *vStore, int Level)
static int	Ivy_NodeBalanceFindLeft (Vec_Ptr_t *vSuper)
static void	Ivy_NodeBalancePermute (Ivy_Man_t *p, Vec_Ptr_t *vSuper, int LeftBound, int fExor)
static void	Ivy_NodeBalancePushUniqueOrderByLevel (Vec_Ptr_t *vStore, Ivy_Obj_t *pObj)
Ivy_Man_t *	Ivy_ManBalance (Ivy_Man_t *p, int fUpdateLevel)
	FUNCTION DEFINITIONS ///. More...
int	Ivy_NodeCompareLevelsDecrease (Ivy_Obj_t **pp1, Ivy_Obj_t **pp2)
Ivy_Obj_t *	Ivy_NodeBalanceBuildSuper (Ivy_Man_t *p, Vec_Ptr_t *vSuper, Ivy_Type_t Type, int fUpdateLevel)
int	Ivy_NodeBalanceCone_rec (Ivy_Obj_t *pRoot, Ivy_Obj_t *pObj, Vec_Ptr_t *vSuper)

Function Documentation

Ivy_Man_t* Ivy_ManBalance	(	Ivy_Man_t *	p,
		int	fUpdateLevel
	)

FUNCTION DEFINITIONS ///.

FUNCTION DECLARATIONS ///.

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

Synopsis [Performs algebraic balancing of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 51 of file ivyBalance.c.

{
    Ivy_Man_t * pNew;
    Ivy_Obj_t * pObj, * pDriver;
    Vec_Vec_t * vStore;
    int i, NewNodeId;
    // clean the old manager
    Ivy_ManCleanTravId( p );
    // create the new manager 
    pNew = Ivy_ManStart();
    // map the nodes
    Ivy_ManConst1(p)->TravId = Ivy_EdgeFromNode( Ivy_ManConst1(pNew) );
    Ivy_ManForEachPi( p, pObj, i )
        pObj->TravId = Ivy_EdgeFromNode( Ivy_ObjCreatePi(pNew) );
    // if HAIG is defined, trasfer the pointers to the PIs/latches
//    if ( p->pHaig )
//        Ivy_ManHaigTrasfer( p, pNew );
    // balance the AIG
    vStore = Vec_VecAlloc( 50 );
    Ivy_ManForEachPo( p, pObj, i )
    {
        pDriver   = Ivy_ObjReal( Ivy_ObjChild0(pObj) );
        NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular(pDriver), vStore, 0, fUpdateLevel );
        NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement(pDriver) );
        Ivy_ObjCreatePo( pNew, Ivy_EdgeToNode(pNew, NewNodeId) );
    }
    Vec_VecFree( vStore );
    if ( (i = Ivy_ManCleanup( pNew )) )
    {
//        printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
    }
    // check the resulting AIG
    if ( !Ivy_ManCheck(pNew) )
        printf( "Ivy_ManBalance(): The check has failed.\n" );
    return pNew;
}

int Ivy_NodeBalance_rec ( Ivy_Man_t *  pNew, Ivy_Obj_t *  pObjOld, Vec_Vec_t *  vStore, int  Level, int  fUpdateLevel  )

static

DECLARATIONS ///.

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

FileName [ivyBalance.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis [Algebraic AIG balancing.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]

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

Synopsis [Returns the ID of new node constructed.]

Description []

SideEffects []

SeeAlso []

Definition at line 125 of file ivyBalance.c.

{
    Ivy_Obj_t * pObjNew;
    Vec_Ptr_t * vSuper;
    int i, NewNodeId;
    assert( !Ivy_IsComplement(pObjOld) );
    assert( !Ivy_ObjIsBuf(pObjOld) );
    // return if the result is known
    if ( Ivy_ObjIsConst1(pObjOld) )
        return pObjOld->TravId;
    if ( pObjOld->TravId )
        return pObjOld->TravId;
    assert( Ivy_ObjIsNode(pObjOld) );
    // get the implication supergate
    vSuper = Ivy_NodeBalanceCone( pObjOld, vStore, Level );
    if ( vSuper->nSize == 0 )
    { // it means that the supergate contains two nodes in the opposite polarity
        pObjOld->TravId = Ivy_EdgeFromNode( Ivy_ManConst0(pNew) );
        return pObjOld->TravId;
    }
    if ( vSuper->nSize < 2 )
        printf( "BUG!\n" );
    // for each old node, derive the new well-balanced node
    for ( i = 0; i < vSuper->nSize; i++ )
    {
        NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular((Ivy_Obj_t *)vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
        NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement((Ivy_Obj_t *)vSuper->pArray[i]) );
        vSuper->pArray[i] = Ivy_EdgeToNode( pNew, NewNodeId );
    }
    // build the supergate
    pObjNew = Ivy_NodeBalanceBuildSuper( pNew, vSuper, Ivy_ObjType(pObjOld), fUpdateLevel );
    vSuper->nSize = 0;
    // make sure the balanced node is not assigned
    assert( pObjOld->TravId == 0 );
    pObjOld->TravId = Ivy_EdgeFromNode( pObjNew );
//    assert( pObjOld->Level >= Ivy_Regular(pObjNew)->Level );
    return pObjOld->TravId;
}

Ivy_Obj_t* Ivy_NodeBalanceBuildSuper	(	Ivy_Man_t *	p,
		Vec_Ptr_t *	vSuper,
		Ivy_Type_t	Type,
		int	fUpdateLevel
	)

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

Synopsis [Builds implication supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 175 of file ivyBalance.c.

{
    Ivy_Obj_t * pObj1, * pObj2;
    int LeftBound;
    assert( vSuper->nSize > 1 );
    // sort the new nodes by level in the decreasing order
    Vec_PtrSort( vSuper, (int (*)(void))Ivy_NodeCompareLevelsDecrease );
    // balance the nodes
    while ( vSuper->nSize > 1 )
    {
        // find the left bound on the node to be paired
        LeftBound = (!fUpdateLevel)? 0 : Ivy_NodeBalanceFindLeft( vSuper );
        // find the node that can be shared (if no such node, randomize choice)
        Ivy_NodeBalancePermute( p, vSuper, LeftBound, Type == IVY_EXOR );
        // pull out the last two nodes
        pObj1 = (Ivy_Obj_t *)Vec_PtrPop(vSuper);
        pObj2 = (Ivy_Obj_t *)Vec_PtrPop(vSuper);
        Ivy_NodeBalancePushUniqueOrderByLevel( vSuper, Ivy_Oper(p, pObj1, pObj2, Type) );
    }
    return (Ivy_Obj_t *)Vec_PtrEntry(vSuper, 0);
}

Vec_Ptr_t * Ivy_NodeBalanceCone ( Ivy_Obj_t *  pObj, Vec_Vec_t *  vStore, int  Level  )

static

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

Synopsis [Collects the nodes of the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 254 of file ivyBalance.c.

{
    Vec_Ptr_t * vNodes;
    int RetValue, i;
    assert( !Ivy_IsComplement(pObj) );
    // extend the storage
    if ( Vec_VecSize( vStore ) <= Level )
        Vec_VecPush( vStore, Level, 0 );
    // get the temporary array of nodes
    vNodes = Vec_VecEntry( vStore, Level );
    Vec_PtrClear( vNodes );
    // collect the nodes in the implication supergate
    RetValue = Ivy_NodeBalanceCone_rec( pObj, pObj, vNodes );
    assert( vNodes->nSize > 1 );
    // unmark the visited nodes
    Vec_PtrForEachEntry( Ivy_Obj_t *, vNodes, pObj, i )
        Ivy_Regular(pObj)->fMarkB = 0;
    // if we found the node and its complement in the same implication supergate, 
    // return empty set of nodes (meaning that we should use constant-0 node)
    if ( RetValue == -1 )
        vNodes->nSize = 0;
    return vNodes;
}

int Ivy_NodeBalanceCone_rec	(	Ivy_Obj_t *	pRoot,
		Ivy_Obj_t *	pObj,
		Vec_Ptr_t *	vSuper
	)

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

Synopsis [Collects the nodes of the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 208 of file ivyBalance.c.

{
    int RetValue1, RetValue2, i;
    // check if the node is visited
    if ( Ivy_Regular(pObj)->fMarkB )
    {
        // check if the node occurs in the same polarity
        for ( i = 0; i < vSuper->nSize; i++ )
            if ( vSuper->pArray[i] == pObj )
                return 1;
        // check if the node is present in the opposite polarity
        for ( i = 0; i < vSuper->nSize; i++ )
            if ( vSuper->pArray[i] == Ivy_Not(pObj) )
                return -1;
        assert( 0 );
        return 0;
    }
    // if the new node is complemented or a PI, another gate begins
    if ( pObj != pRoot && (Ivy_IsComplement(pObj) || Ivy_ObjType(pObj) != Ivy_ObjType(pRoot) || Ivy_ObjRefs(pObj) > 1 || Vec_PtrSize(vSuper) > 10000) )
    {
        Vec_PtrPush( vSuper, pObj );
        Ivy_Regular(pObj)->fMarkB = 1;
        return 0;
    }
    assert( !Ivy_IsComplement(pObj) );
    assert( Ivy_ObjIsNode(pObj) );
    // go through the branches
    RetValue1 = Ivy_NodeBalanceCone_rec( pRoot, Ivy_ObjReal( Ivy_ObjChild0(pObj) ), vSuper );
    RetValue2 = Ivy_NodeBalanceCone_rec( pRoot, Ivy_ObjReal( Ivy_ObjChild1(pObj) ), vSuper );
    if ( RetValue1 == -1 || RetValue2 == -1 )
        return -1;
    // return 1 if at least one branch has a duplicate
    return RetValue1 || RetValue2;
}

int Ivy_NodeBalanceFindLeft ( Vec_Ptr_t *  vSuper )

static

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

Synopsis [Finds the left bound on the next candidate to be paired.]

Description [The nodes in the array are in the decreasing order of levels. The last node in the array has the smallest level. By default it would be paired with the next node on the left. However, it may be possible to pair it with some other node on the left, in such a way that the new node is shared. This procedure finds the index of the left-most node, which can be paired with the last node.]

SideEffects []

SeeAlso []

Definition at line 293 of file ivyBalance.c.

{
    Ivy_Obj_t * pObjRight, * pObjLeft;
    int Current;
    // if two or less nodes, pair with the first
    if ( Vec_PtrSize(vSuper) < 3 )
        return 0;
    // set the pointer to the one before the last
    Current = Vec_PtrSize(vSuper) - 2;
    pObjRight = (Ivy_Obj_t *)Vec_PtrEntry( vSuper, Current );
    // go through the nodes to the left of this one
    for ( Current--; Current >= 0; Current-- )
    {
        // get the next node on the left
        pObjLeft = (Ivy_Obj_t *)Vec_PtrEntry( vSuper, Current );
        // if the level of this node is different, quit the loop
        if ( Ivy_Regular(pObjLeft)->Level != Ivy_Regular(pObjRight)->Level )
            break;
    }
    Current++;    
    // get the node, for which the equality holds
    pObjLeft = (Ivy_Obj_t *)Vec_PtrEntry( vSuper, Current );
    assert( Ivy_Regular(pObjLeft)->Level == Ivy_Regular(pObjRight)->Level );
    return Current;
}

void Ivy_NodeBalancePermute ( Ivy_Man_t *  p, Vec_Ptr_t *  vSuper, int  LeftBound, int  fExor  )

static

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

Synopsis [Moves closer to the end the node that is best for sharing.]

Description [If there is no node with sharing, randomly chooses one of the legal nodes.]

SideEffects []

SeeAlso []

Definition at line 331 of file ivyBalance.c.

{
    Ivy_Obj_t * pObj1, * pObj2, * pObj3, * pGhost;
    int RightBound, i;
    // get the right bound
    RightBound = Vec_PtrSize(vSuper) - 2;
    assert( LeftBound <= RightBound );
    if ( LeftBound == RightBound )
        return;
    // get the two last nodes
    pObj1 = (Ivy_Obj_t *)Vec_PtrEntry( vSuper, RightBound + 1 );
    pObj2 = (Ivy_Obj_t *)Vec_PtrEntry( vSuper, RightBound     );
    if ( Ivy_Regular(pObj1) == p->pConst1 || Ivy_Regular(pObj2) == p->pConst1 )
        return;
    // find the first node that can be shared
    for ( i = RightBound; i >= LeftBound; i-- )
    {
        pObj3 = (Ivy_Obj_t *)Vec_PtrEntry( vSuper, i );
        if ( Ivy_Regular(pObj3) == p->pConst1 )
        {
            Vec_PtrWriteEntry( vSuper, i,          pObj2 );
            Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
            return;
        }
        pGhost = Ivy_ObjCreateGhost( p, pObj1, pObj3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE );
        if ( Ivy_TableLookup( p, pGhost ) )
        {
            if ( pObj3 == pObj2 )
                return;
            Vec_PtrWriteEntry( vSuper, i,          pObj2 );
            Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
            return;
        }
    }
/*
    // we did not find the node to share, randomize choice
    {
        int Choice = rand() % (RightBound - LeftBound + 1);
        pObj3 = Vec_PtrEntry( vSuper, LeftBound + Choice );
        if ( pObj3 == pObj2 )
            return;
        Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pObj2 );
        Vec_PtrWriteEntry( vSuper, RightBound,         pObj3 );
    }
*/
}

void Ivy_NodeBalancePushUniqueOrderByLevel ( Vec_Ptr_t *  vStore, Ivy_Obj_t *  pObj  )

static

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

Synopsis [Inserts a new node in the order by levels.]

Description []

SideEffects []

SeeAlso []

Definition at line 389 of file ivyBalance.c.

{
    Ivy_Obj_t * pObj1, * pObj2;
    int i;
    if ( Vec_PtrPushUnique(vStore, pObj) )
        return;
    // find the p of the node
    for ( i = vStore->nSize-1; i > 0; i-- )
    {
        pObj1 = (Ivy_Obj_t *)vStore->pArray[i  ];
        pObj2 = (Ivy_Obj_t *)vStore->pArray[i-1];
        if ( Ivy_Regular(pObj1)->Level <= Ivy_Regular(pObj2)->Level )
            break;
        vStore->pArray[i  ] = pObj2;
        vStore->pArray[i-1] = pObj1;
    }
}

int Ivy_NodeCompareLevelsDecrease	(	Ivy_Obj_t **	pp1,
		Ivy_Obj_t **	pp2
	)

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

Synopsis [Procedure used for sorting the nodes in decreasing order of levels.]

Description []

SideEffects []

SeeAlso []

Definition at line 99 of file ivyBalance.c.

{
    int Diff = Ivy_Regular(*pp1)->Level - Ivy_Regular(*pp2)->Level;
    if ( Diff > 0 )
        return -1;
    if ( Diff < 0 ) 
        return 1;
    Diff = Ivy_Regular(*pp1)->Id - Ivy_Regular(*pp2)->Id;
    if ( Diff > 0 )
        return -1;
    if ( Diff < 0 ) 
        return 1;
    return 0; 
}