bbr.h File Reference

#include <stdio.h>
#include "aig/aig/aig.h"
#include "aig/saig/saig.h"
#include "bdd/cudd/cuddInt.h"

Include dependency graph for bbr.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Typedefs
typedef struct Bbr_ImageTree_t_	Bbr_ImageTree_t
	FUNCTION DECLARATIONS ///.
typedef struct Bbr_ImageTree2_t_	Bbr_ImageTree2_t

Functions
Bbr_ImageTree_t *	Bbr_bddImageStart (DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int nBddMax, int fVerbose)
DdNode *	Bbr_bddImageCompute (Bbr_ImageTree_t *pTree, DdNode *bCare)
void	Bbr_bddImageTreeDelete (Bbr_ImageTree_t *pTree)
DdNode *	Bbr_bddImageRead (Bbr_ImageTree_t *pTree)
Bbr_ImageTree2_t *	Bbr_bddImageStart2 (DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int fVerbose)
DdNode *	Bbr_bddImageCompute2 (Bbr_ImageTree2_t *pTree, DdNode *bCare)
void	Bbr_bddImageTreeDelete2 (Bbr_ImageTree2_t *pTree)
DdNode *	Bbr_bddImageRead2 (Bbr_ImageTree2_t *pTree)
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)
int	Aig_ManVerifyUsingBdds (Aig_Man_t *p, Saig_ParBbr_t *pPars)
void	Bbr_ManSetDefaultParams (Saig_ParBbr_t *p)
	FUNCTION DEFINITIONS ///.

Typedef Documentation

Bbr_ImageTree2_t

typedef struct Bbr_ImageTree2_t_ Bbr_ImageTree2_t

Definition at line 66 of file bbr.h.

Bbr_ImageTree_t

typedef struct Bbr_ImageTree_t_ Bbr_ImageTree_t

FUNCTION DECLARATIONS ///.

Definition at line 58 of file bbr.h.

Function Documentation

Aig_ManComputeGlobalBdds()

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

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Aig_ManFreeGlobalBdds()

void Aig_ManFreeGlobalBdds ( Aig_Man_t * p, DdManager * dd )

extern

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 );
}

Here is the caller graph for this function:

Aig_ManSizeOfGlobalBdds()

int Aig_ManSizeOfGlobalBdds ( Aig_Man_t * p )

extern

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;
}

Aig_ManVerifyUsingBdds()

int Aig_ManVerifyUsingBdds ( Aig_Man_t * pInit, Saig_ParBbr_t * pPars )

extern

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

Synopsis [Performs reachability to see if any PO can be asserted.]

Description []

SideEffects []

SeeAlso []

Definition at line 592 of file saigDup.c.

{ return 0; }

Here is the call graph for this function:

Here is the caller graph for this function:

Bbr_bddImageCompute()

DdNode * Bbr_bddImageCompute ( Bbr_ImageTree_t * pTree, DdNode * bCare )

extern

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

Synopsis [Compute the image.]

Description []

SideEffects []

SeeAlso []

Definition at line 253 of file bbrImage.c.

{
    DdManager * dd = pTree->pCare->dd;
    DdNode * bSupp, * bRem;
 
    pTree->nIter++;
 
    // make sure the supports are okay
    bSupp = Cudd_Support( dd, bCare );        Cudd_Ref( bSupp );
    if ( bSupp != pTree->bCareSupp )
    {
        bRem = Cudd_bddExistAbstract( dd, bSupp, pTree->bCareSupp );  Cudd_Ref( bRem );
        if ( bRem != b1 )
        {
printf( "Original care set support: " );
ABC_PRB( dd, pTree->bCareSupp );
printf( "Current care set support: " );
ABC_PRB( dd, bSupp );
            Cudd_RecursiveDeref( dd, bSupp );
            Cudd_RecursiveDeref( dd, bRem );
            printf( "The care set depends on some vars that were not in the care set during scheduling.\n" );
            return NULL;
        }
        Cudd_RecursiveDeref( dd, bRem );
    }
    Cudd_RecursiveDeref( dd, bSupp );
 
    // remove the previous image
    Cudd_RecursiveDeref( dd, pTree->pCare->bImage );
    pTree->pCare->bImage = bCare;   Cudd_Ref( bCare );
 
    // compute the image
    pTree->nNodesMax = 0;
    if ( !Bbr_bddImageCompute_rec( pTree, pTree->pRoot ) )
        return NULL;
    if ( pTree->nNodesMaxT < pTree->nNodesMax )
        pTree->nNodesMaxT = pTree->nNodesMax;
 
//    if ( pTree->fVerbose )
//        printf( "Iter %2d : Max nodes = %5d.\n", pTree->nIter, pTree->nNodesMax );
    return pTree->pRoot->bImage;
}

Here is the caller graph for this function:

Bbr_bddImageCompute2()

DdNode * Bbr_bddImageCompute2 ( Bbr_ImageTree2_t * pTree, DdNode * bCare )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1273 of file bbrImage.c.

{
    if ( pTree->bImage )
        Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
    pTree->bImage = Cudd_bddAndAbstract( pTree->dd, pTree->bRel, bCare, pTree->bCube ); 
    Cudd_Ref( pTree->bImage );
    return pTree->bImage;
}

Here is the caller graph for this function:

Bbr_bddImageRead()

DdNode * Bbr_bddImageRead ( Bbr_ImageTree_t * pTree )

extern

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

Synopsis [Reads the image from the tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 326 of file bbrImage.c.

{
    return pTree->pRoot->bImage;
}

Bbr_bddImageRead2()

DdNode * Bbr_bddImageRead2 ( Bbr_ImageTree2_t * pTree )

extern

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

Synopsis [Returns the previously computed image.]

Description []

SideEffects []

SeeAlso []

Definition at line 1315 of file bbrImage.c.

{
    return pTree->bImage;
}

Bbr_bddImageStart()

Bbr_ImageTree_t * Bbr_bddImageStart ( DdManager * dd, DdNode * bCare, int nParts, DdNode ** pbParts, int nVars, DdNode ** pbVars, int nBddMax, int fVerbose )

extern

AutomaticEnd Function*************************************************************

Synopsis [Starts the image computation using tree-based scheduling.]

Description [This procedure starts the image computation. It uses the given care set to test-run the image computation and creates the quantification tree by scheduling variable quantifications. The tree can be used to compute images for other care sets without rescheduling. In this case, Bbr_bddImageCompute() should be called.]

SideEffects []

SeeAlso []

Definition at line 168 of file bbrImage.c.

{
    Bbr_ImageTree_t * pTree;
    Bbr_ImagePart_t ** pParts;
    Bbr_ImageVar_t ** pVars;
    Bbr_ImageNode_t ** pNodes, * pCare;
    int fStop, v;
 
    if ( fVerbose && dd->size <= 80 )
        Bbr_bddImagePrintLatchDependency( dd, bCare, nParts, pbParts, nVars, pbVars );
 
    // create variables, partitions and leaf nodes
    pParts = Bbr_CreateParts( dd, nParts, pbParts, bCare );
    pVars  = Bbr_CreateVars( dd, nParts + 1, pParts, nVars, pbVars );
    pNodes = Bbr_CreateNodes( dd, nParts + 1, pParts, dd->size, pVars );
    pCare  = pNodes[nParts];
 
    // process the nodes
    while ( Bbr_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars, &fStop, nBddMax ) );
 
    // consider the case of BDD node blowup
    if ( fStop )
    {
        for ( v = 0; v < dd->size; v++ )
            if ( pVars[v] )
                ABC_FREE( pVars[v] );
        ABC_FREE( pVars );
        for ( v = 0; v <= nParts; v++ )
            if ( pNodes[v] )
            {
                Bbr_DeleteParts_rec( pNodes[v] );
                Bbr_bddImageTreeDelete_rec( pNodes[v] );
            }
        ABC_FREE( pNodes );
        ABC_FREE( pParts );
        return NULL;
    }
 
    // make sure the variables are gone
    for ( v = 0; v < dd->size; v++ )
        assert( pVars[v] == NULL );
    ABC_FREE( pVars );
    
    // create the tree
    pTree = ABC_ALLOC( Bbr_ImageTree_t, 1 );
    memset( pTree, 0, sizeof(Bbr_ImageTree_t) );
    pTree->pCare = pCare;
    pTree->nBddMax = nBddMax;
    pTree->fVerbose = fVerbose;
 
    // merge the topmost nodes
    while ( (pTree->pRoot = Bbr_MergeTopNodes( dd, nParts + 1, pNodes )) == NULL );
 
    // make sure the nodes are gone
    for ( v = 0; v < nParts + 1; v++ )
        assert( pNodes[v] == NULL );
    ABC_FREE( pNodes );
 
//    if ( fVerbose )
//        Bbr_bddImagePrintTree( pTree );
 
    // set the support of the care set
    pTree->bCareSupp = Cudd_Support( dd, bCare );  Cudd_Ref( pTree->bCareSupp );
 
    // clean the partitions
    Bbr_DeleteParts_rec( pTree->pRoot );
    ABC_FREE( pParts );
 
    return pTree;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Bbr_bddImageStart2()

Bbr_ImageTree2_t * Bbr_bddImageStart2 ( DdManager * dd, DdNode * bCare, int nParts, DdNode ** pbParts, int nVars, DdNode ** pbVars, int fVerbose )

extern

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

Synopsis [Starts the monolithic image computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1231 of file bbrImage.c.

{
    Bbr_ImageTree2_t * pTree;
    DdNode * bCubeAll, * bCubeNot, * bTemp;
    int i;
 
    pTree = ABC_ALLOC( Bbr_ImageTree2_t, 1 );
    pTree->dd = dd;
    pTree->bImage = NULL;
 
    bCubeAll = Bbr_bddComputeCube( dd, dd->vars, dd->size );      Cudd_Ref( bCubeAll );
    bCubeNot = Bbr_bddComputeCube( dd, pbVars,   nVars );         Cudd_Ref( bCubeNot );
    pTree->bCube = Cudd_bddExistAbstract( dd, bCubeAll, bCubeNot ); Cudd_Ref( pTree->bCube );
    Cudd_RecursiveDeref( dd, bCubeAll );
    Cudd_RecursiveDeref( dd, bCubeNot );
 
    // derive the monolithic relation
    pTree->bRel = b1;   Cudd_Ref( pTree->bRel );
    for ( i = 0; i < nParts; i++ )
    {
        pTree->bRel = Cudd_bddAnd( dd, bTemp = pTree->bRel, pbParts[i] ); Cudd_Ref( pTree->bRel );
        Cudd_RecursiveDeref( dd, bTemp );
    }
    Bbr_bddImageCompute2( pTree, bCare );
    return pTree;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Bbr_bddImageTreeDelete()

void Bbr_bddImageTreeDelete ( Bbr_ImageTree_t * pTree )

extern

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

Synopsis [Delete the tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file bbrImage.c.

{
    if ( pTree->bCareSupp )
        Cudd_RecursiveDeref( pTree->pRoot->dd, pTree->bCareSupp );
    Bbr_bddImageTreeDelete_rec( pTree->pRoot );
    ABC_FREE( pTree );
}

Here is the caller graph for this function:

Bbr_bddImageTreeDelete2()

void Bbr_bddImageTreeDelete2 ( Bbr_ImageTree2_t * pTree )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1293 of file bbrImage.c.

{
    if ( pTree->bRel )
        Cudd_RecursiveDeref( pTree->dd, pTree->bRel );
    if ( pTree->bCube )
        Cudd_RecursiveDeref( pTree->dd, pTree->bCube );
    if ( pTree->bImage )
        Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
    ABC_FREE( pTree );
}

Here is the caller graph for this function:

Bbr_ManSetDefaultParams()

void Bbr_ManSetDefaultParams ( Saig_ParBbr_t * p )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [This procedure sets default resynthesis parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 593 of file saigDup.c.

{}

Here is the call graph for this function:

Here is the caller graph for this function: