llb.h File Reference

Go to the source code of this file.

Data Structures
struct	Gia_ParLlb_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Gia_ParLlb_t_	Gia_ParLlb_t
	INCLUDES ///. More...

Functions
void	Llb_ManSetDefaultParams (Gia_ParLlb_t *pPars)
	MACRO DEFINITIONS ///. More...
int	Llb_Nonlin4CoreReach (Aig_Man_t *pAig, Gia_ParLlb_t *pPars)

Typedef Documentation

typedef typedefABC_NAMESPACE_HEADER_START struct Gia_ParLlb_t_ Gia_ParLlb_t

INCLUDES ///.

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

FileName [llb.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD-based reachability.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 8, 2010.]

Revision [

Id:

llb.h,v 1.00 2010/05/08 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 41 of file llb.h.

Function Documentation

void Llb_ManSetDefaultParams

(

Gia_ParLlb_t *

p

)

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

MACRO DEFINITIONS ///.

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

FileName [llb1Core.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD based reachability.]

Synopsis [Top-level procedure.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file llb1Core.c.

{
    memset( p, 0, sizeof(Gia_ParLlb_t) );
    p->nBddMax       = 10000000;
    p->nIterMax      = 10000000;
    p->nClusterMax   =       20;
    p->nHintDepth    =        0;
    p->HintFirst     =        0;
    p->fUseFlow      =        0;  // use flow 
    p->nVolumeMax    =      100;  // max volume
    p->nVolumeMin    =       30;  // min volume
    p->nPartValue    =        5;  // partitioning value
    p->fBackward     =        0;  // forward by default
    p->fReorder      =        1;
    p->fIndConstr    =        0;
    p->fUsePivots    =        0;
    p->fCluster      =        0;
    p->fSchedule     =        0;
    p->fDumpReached  =        0;
    p->fVerbose      =        0;
    p->fVeryVerbose  =        0;
    p->fSilent       =        0;
    p->TimeLimit     =        0;
//    p->TimeLimit     =        0;
    p->TimeLimitGlo  =        0;
    p->TimeTarget    =        0;
    p->iFrame        =       -1;
}

int Llb_Nonlin4CoreReach	(	Aig_Man_t *	pAig,
		Gia_ParLlb_t *	pPars
	)

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

Synopsis [Finds balanced cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 1067 of file llb4Nonlin.c.

{
    Llb_Mnx_t * pMnn;
    int RetValue = -1;
    if ( pPars->fVerbose )
    Aig_ManPrintStats( pAig );
    if ( pPars->fCluster && Aig_ManObjNum(pAig) >= (1 << 15) )
    {
        printf( "The number of objects is more than 2^15.  Clustering cannot be used.\n" );
        return RetValue;
    }
    {
        abctime clk = Abc_Clock();
        pMnn = Llb_MnxStart( pAig, pPars );
//Llb_MnxCheckNextStateVars( pMnn );
        if ( !pPars->fSkipReach )
            RetValue = Llb_Nonlin4Reachability( pMnn );
        pMnn->timeTotal = Abc_Clock() - clk;
        Llb_MnxStop( pMnn );
    }
    return RetValue;
}