bbrImage.c File Reference

#include "bbr.h"
#include "bdd/mtr/mtr.h"

Include dependency graph for bbrImage.c:

Go to the source code of this file.

Classes
struct	Bbr_ImageTree_t_
struct	Bbr_ImageNode_t_
struct	Bbr_ImagePart_t_
struct	Bbr_ImageVar_t_
struct	Bbr_ImageTree2_t_

Macros
#define	b0   Cudd_Not((dd)->one)
#define	b1   (dd)->one
#define	ABC_PRB(dd, f)

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Bbr_ImageNode_t_	Bbr_ImageNode_t
typedef struct Bbr_ImagePart_t_	Bbr_ImagePart_t
typedef struct Bbr_ImageVar_t_	Bbr_ImageVar_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)
DdNode *	Bbr_bddComputeCube (DdManager *dd, DdNode **bXVars, int nVars)
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)

Macro Definition Documentation

ABC_PRB

#define ABC_PRB	(		dd,
			f )

Value:

printf("%s = ", #f); Bbr_bddPrint(dd,f); printf("\n")

Definition at line 100 of file bbrImage.c.

b0

#define b0   Cudd_Not((dd)->one)

Definition at line 96 of file bbrImage.c.

b1

#define b1   (dd)->one

Definition at line 97 of file bbrImage.c.

Typedef Documentation

Bbr_ImageNode_t

typedef typedefABC_NAMESPACE_IMPL_START struct Bbr_ImageNode_t_ Bbr_ImageNode_t

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

FileName [bbrImage.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD-based reachability analysis.]

Synopsis [Performs image computation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

]

Definition at line 42 of file bbrImage.c.

Bbr_ImagePart_t

typedef struct Bbr_ImagePart_t_ Bbr_ImagePart_t

Definition at line 43 of file bbrImage.c.

Bbr_ImageVar_t

typedef struct Bbr_ImageVar_t_ Bbr_ImageVar_t

Definition at line 44 of file bbrImage.c.

Function Documentation

Bbr_bddComputeCube()

DdNode * Bbr_bddComputeCube	(	DdManager *	dd,
		DdNode **	bXVars,
		int	nVars )

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

Synopsis [Computes the positive polarty cube composed of the first vars in the array.]

Description []

SideEffects []

SeeAlso []

Definition at line 1191 of file bbrImage.c.

{
    DdNode * bRes;
    DdNode * bTemp;
    int i;
 
    bRes = b1; Cudd_Ref( bRes );
    for ( i = 0; i < nVars; i++ )
    {
        bRes = Cudd_bddAnd( dd, bTemp = bRes, bXVars[i] );  Cudd_Ref( bRes );
        Cudd_RecursiveDeref( dd, bTemp );
    }
 
    Cudd_Deref( bRes );
    return bRes;
}

Here is the caller graph for this function:

Bbr_bddImageCompute()

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

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 )

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

)

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

)

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 )

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 )

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

)

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

)

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: