bbr.h File Reference

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

Go to the source code of this file.

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

Functions
static ABC_NAMESPACE_HEADER_START DdNode *	Aig_ObjGlobalBdd (Aig_Obj_t *pObj)
	INCLUDES ///. More...
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 ///. More...

Typedef Documentation

typedef struct Bbr_ImageTree2_t_ Bbr_ImageTree2_t

Definition at line 66 of file bbr.h.

typedef struct Bbr_ImageTree_t_ Bbr_ImageTree_t

FUNCTION DECLARATIONS ///.

Definition at line 58 of file bbr.h.

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

int Aig_ManVerifyUsingBdds	(	Aig_Man_t *	pInit,
		Saig_ParBbr_t *	pPars
	)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 544 of file bbrReach.c.

{
    Abc_Cex_t * pCexOld, * pCexNew;
    Aig_Man_t * p;
    Aig_Obj_t * pObj;
    Vec_Int_t * vInputMap;
    int i, k, Entry, iBitOld, iBitNew, RetValue;
//    pPars->fVerbose = 1;
    // check if there are PIs without fanout
    Saig_ManForEachPi( pInit, pObj, i )
        if ( Aig_ObjRefs(pObj) == 0 )
            break;
    if ( i == Saig_ManPiNum(pInit) )
        return Aig_ManVerifyUsingBdds_int( pInit, pPars );
    // create new AIG
    p = Aig_ManDupTrim( pInit );
    assert( Aig_ManCiNum(p) < Aig_ManCiNum(pInit) );
    assert( Aig_ManRegNum(p) == Aig_ManRegNum(pInit) );
    RetValue = Aig_ManVerifyUsingBdds_int( p, pPars );
    if ( RetValue != 0 )
    {
        Aig_ManStop( p );
        return RetValue;
    }
    // the problem is satisfiable - remap the pattern
    pCexOld = p->pSeqModel;
    assert( pCexOld != NULL );
    // create input map
    vInputMap = Vec_IntAlloc( Saig_ManPiNum(pInit) );
    Saig_ManForEachPi( pInit, pObj, i )
        if ( pObj->pData != NULL )
            Vec_IntPush( vInputMap, Aig_ObjCioId((Aig_Obj_t *)pObj->pData) );
        else
            Vec_IntPush( vInputMap, -1 );
    // create new pattern
    pCexNew = Abc_CexAlloc( Saig_ManRegNum(pInit), Saig_ManPiNum(pInit), pCexOld->iFrame+1 );
    pCexNew->iFrame = pCexOld->iFrame;
    pCexNew->iPo    = pCexOld->iPo;
    // copy the bit-data
    for ( iBitOld = 0; iBitOld < pCexOld->nRegs; iBitOld++ )
        if ( Abc_InfoHasBit( pCexOld->pData, iBitOld ) )
            Abc_InfoSetBit( pCexNew->pData, iBitOld );
    // copy the primary input data
    iBitNew = iBitOld;
    for ( i = 0; i <= pCexNew->iFrame; i++ )
    {
        Vec_IntForEachEntry( vInputMap, Entry, k )
        {
            if ( Entry == -1 )
                continue;
            if ( Abc_InfoHasBit( pCexOld->pData, iBitOld + Entry ) )
                Abc_InfoSetBit( pCexNew->pData, iBitNew + k );
        }
        iBitOld += Saig_ManPiNum(p);
        iBitNew += Saig_ManPiNum(pInit);
    }
    assert( iBitOld < iBitNew );
    assert( iBitOld == pCexOld->nBits );
    assert( iBitNew == pCexNew->nBits );
    Vec_IntFree( vInputMap );
    pInit->pSeqModel = pCexNew;
    Aig_ManStop( p );
    return 0;
}

static ABC_NAMESPACE_HEADER_START DdNode* Aig_ObjGlobalBdd ( Aig_Obj_t *  pObj )

inlinestatic

INCLUDES ///.

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

FileName [bbr.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD-based reachability analysis.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

bbr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///MACRO DEFINITIONS ///

Definition at line 51 of file bbr.h.

{ return (DdNode *)pObj->pData; }

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

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

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

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

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

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

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

void Bbr_ManSetDefaultParams

(

Saig_ParBbr_t *

p

)

FUNCTION DEFINITIONS ///.

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

Synopsis [This procedure sets default resynthesis parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 49 of file bbrReach.c.

{
    memset( p, 0, sizeof(Saig_ParBbr_t) );
    p->TimeLimit     =     0;
    p->nBddMax       = 50000;
    p->nIterMax      =  1000;
    p->fPartition    =     1;
    p->fReorder      =     1;
    p->fReorderImage =     1;
    p->fVerbose      =     0;
    p->fSilent       =     0;
    p->iFrame        =    -1;
}