bbrNtbdd.c File Reference

#include "bbr.h"

Go to the source code of this file.

Functions
static void	Aig_ObjSetGlobalBdd (Aig_Obj_t *pObj, DdNode *bFunc)
	DECLARATIONS ///. More...
static void	Aig_ObjCleanGlobalBdd (DdManager *dd, Aig_Obj_t *pObj)
DdNode *	Bbr_NodeGlobalBdds_rec (DdManager *dd, Aig_Obj_t *pNode, int nBddSizeMax, int fDropInternal, ProgressBar *pProgress, int *pCounter, int fVerbose)
	FUNCTION DEFINITIONS ///. More...
void	Aig_ManFreeGlobalBdds (Aig_Man_t *p, DdManager *dd)
int	Aig_ManSizeOfGlobalBdds (Aig_Man_t *p)
DdManager *	Aig_ManComputeGlobalBdds (Aig_Man_t *p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose)

Variables
ABC_NAMESPACE_IMPL_START typedef char	ProgressBar

Function Documentation

DdManager* Aig_ManComputeGlobalBdds	(	Aig_Man_t *	p,
		int	nBddSizeMax,
		int	fDropInternal,
		int	fReorder,
		int	fVerbose
	)

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

Synopsis [Recursively computes global BDDs for the AIG in the manager.]

Description [On exit, BDDs are stored in the pNode->pData fields.]

SideEffects []

SeeAlso []

Definition at line 157 of file bbrNtbdd.c.

{
    ProgressBar * pProgress = NULL;
    Aig_Obj_t * pObj;
    DdManager * dd;
    DdNode * bFunc;
    int i, Counter;
    // start the manager
    dd = Cudd_Init( Aig_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    // set reordering
    if ( fReorder )
        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
    // prepare to construct global BDDs
    Aig_ManCleanData( p );
    // assign the constant node BDD
    Aig_ObjSetGlobalBdd( Aig_ManConst1(p), dd->one );   Cudd_Ref( dd->one );
    // set the elementary variables
    Aig_ManForEachCi( p, pObj, i )
    {
        Aig_ObjSetGlobalBdd( pObj, dd->vars[i] );  Cudd_Ref( dd->vars[i] );
    }

    // collect the global functions of the COs
    Counter = 0;
    // construct the BDDs
//    pProgress = Extra_ProgressBarStart( stdout, Aig_ManNodeNum(p) );
    Aig_ManForEachCo( p, pObj, i )
    {
        bFunc = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin0(pObj), nBddSizeMax, fDropInternal, pProgress, &Counter, fVerbose );
        if ( bFunc == NULL )
        {
            if ( fVerbose )
            printf( "Constructing global BDDs is aborted.\n" );
            Aig_ManFreeGlobalBdds( p, dd );
            Cudd_Quit( dd ); 
            // reset references
            Aig_ManResetRefs( p );
            return NULL;
        }
        bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pObj) );  Cudd_Ref( bFunc ); 
        Aig_ObjSetGlobalBdd( pObj, bFunc );
    }
//    Extra_ProgressBarStop( pProgress );
    // reset references
    Aig_ManResetRefs( p );
    // reorder one more time
    if ( fReorder )
    {
        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
        Cudd_AutodynDisable( dd );
    }
//    Cudd_PrintInfo( dd, stdout );
    return dd;
}

void Aig_ManFreeGlobalBdds	(	Aig_Man_t *	p,
		DdManager *	dd
	)

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

Synopsis [Frees the global BDDs of the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 112 of file bbrNtbdd.c.

{ 
    Aig_Obj_t * pObj;
    int i;
    Aig_ManForEachObj( p, pObj, i )
        if ( Aig_ObjGlobalBdd(pObj) )
            Aig_ObjCleanGlobalBdd( dd, pObj );
}

int Aig_ManSizeOfGlobalBdds

(

Aig_Man_t *

p

)

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

Synopsis [Returns the shared size of global BDDs of the COs.]

Description []

SideEffects []

SeeAlso []

Definition at line 132 of file bbrNtbdd.c.

{
    Vec_Ptr_t * vFuncsGlob;
    Aig_Obj_t * pObj;
    int RetValue, i;
    // complement the global functions
    vFuncsGlob = Vec_PtrAlloc( Aig_ManCoNum(p) );
    Aig_ManForEachCo( p, pObj, i )
        Vec_PtrPush( vFuncsGlob, Aig_ObjGlobalBdd(pObj) );
    RetValue = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncsGlob), Vec_PtrSize(vFuncsGlob) );
    Vec_PtrFree( vFuncsGlob );
    return RetValue;
}

static void Aig_ObjCleanGlobalBdd ( DdManager *  dd, Aig_Obj_t *  pObj  )

inlinestatic

Definition at line 34 of file bbrNtbdd.c.

{ Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); pObj->pData = NULL; }

static void Aig_ObjSetGlobalBdd ( Aig_Obj_t *  pObj, DdNode *  bFunc  )

inlinestatic

DECLARATIONS ///.

Definition at line 33 of file bbrNtbdd.c.

{ pObj->pData = bFunc; }

DdNode* Bbr_NodeGlobalBdds_rec	(	DdManager *	dd,
		Aig_Obj_t *	pNode,
		int	nBddSizeMax,
		int	fDropInternal,
		ProgressBar *	pProgress,
		int *	pCounter,
		int	fVerbose
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Derives the global BDD for one AIG node.]

Description []

SideEffects []

SeeAlso []

Definition at line 51 of file bbrNtbdd.c.

{
    DdNode * bFunc, * bFunc0, * bFunc1;
    assert( !Aig_IsComplement(pNode) );
    if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
    {
//        Extra_ProgressBarStop( pProgress );
        if ( fVerbose )
        printf( "The number of live nodes reached %d.\n", nBddSizeMax );
        fflush( stdout );
        return NULL;
    }
    // if the result is available return
    if ( Aig_ObjGlobalBdd(pNode) == NULL )
    {
        // compute the result for both branches
        bFunc0 = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin0(pNode), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
        if ( bFunc0 == NULL )
            return NULL;
        Cudd_Ref( bFunc0 );
        bFunc1 = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin1(pNode), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
        if ( bFunc1 == NULL )
            return NULL;
        Cudd_Ref( bFunc1 );
        bFunc0 = Cudd_NotCond( bFunc0, Aig_ObjFaninC0(pNode) );
        bFunc1 = Cudd_NotCond( bFunc1, Aig_ObjFaninC1(pNode) );
        // get the final result
        bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );
        Cudd_RecursiveDeref( dd, bFunc0 );
        Cudd_RecursiveDeref( dd, bFunc1 );
        // add the number of used nodes
        (*pCounter)++;
        // set the result
        assert( Aig_ObjGlobalBdd(pNode) == NULL );
        Aig_ObjSetGlobalBdd( pNode, bFunc );
        // increment the progress bar
//        if ( pProgress )
//            Extra_ProgressBarUpdate( pProgress, *pCounter, NULL );
    }
    // prepare the return value
    bFunc = Aig_ObjGlobalBdd(pNode);
    // dereference BDD at the node
    if ( --pNode->nRefs == 0 && fDropInternal )
    {
        Cudd_Deref( bFunc );
        Aig_ObjSetGlobalBdd( pNode, NULL );
    }
    return bFunc;
}

Variable Documentation

ABC_NAMESPACE_IMPL_START typedef char ProgressBar

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

FileName [bbrNtbdd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD-based reachability analysis.]

Synopsis [Procedures to construct global BDDs for the network.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

bbrNtbdd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 27 of file bbrNtbdd.c.