llb1Core.c File Reference

#include "llbInt.h"
#include "aig/gia/gia.h"
#include "aig/gia/giaAig.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START void	Llb_ManSetDefaultParams (Gia_ParLlb_t *p)
	DECLARATIONS ///. More...
void	Llb_ManPrintAig (Llb_Man_t *p)
int	Llb_ManModelCheckAig (Aig_Man_t *pAigGlo, Gia_ParLlb_t *pPars, Vec_Int_t *vHints, DdManager **pddGlo)
int	Llb_ManModelCheckGia (Gia_Man_t *pGia, Gia_ParLlb_t *pPars)

Function Documentation

int Llb_ManModelCheckAig	(	Aig_Man_t *	pAigGlo,
		Gia_ParLlb_t *	pPars,
		Vec_Int_t *	vHints,
		DdManager **	pddGlo
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 112 of file llb1Core.c.

{
    Llb_Man_t * p = NULL; 
    Aig_Man_t * pAig;
    int RetValue = -1;
    abctime clk = Abc_Clock();

    if ( pPars->fIndConstr )
    {
        assert( vHints == NULL );
        vHints = Llb_ManDeriveConstraints( pAigGlo );
    }

    // derive AIG for hints
    if ( vHints == NULL )
        pAig = Aig_ManDupSimple( pAigGlo );
    else
    {
        if ( pPars->fVerbose )
            Llb_ManPrintEntries( pAigGlo, vHints );
        pAig = Aig_ManDupSimpleWithHints( pAigGlo, vHints );
    }


    if ( pPars->fUseFlow )
    {
//        p = Llb_ManStartFlow( pAigGlo, pAig, pPars );
    }
    else
    {
        p = Llb_ManStart( pAigGlo, pAig, pPars );
        if ( pPars->fVerbose )
        {
            Llb_ManPrintAig( p );
            printf( "Original matrix:          " );
            Llb_MtrPrintMatrixStats( p->pMatrix );
            if ( pPars->fVeryVerbose )
                Llb_MtrPrint( p->pMatrix, 1 );
        }
        if ( pPars->fCluster )
        {
            Llb_ManCluster( p->pMatrix );
            if ( pPars->fVerbose )
            {
                printf( "Matrix after clustering:  " );
                Llb_MtrPrintMatrixStats( p->pMatrix );
                if ( pPars->fVeryVerbose )
                    Llb_MtrPrint( p->pMatrix, 1 );
            }
        }
        if ( pPars->fSchedule )
        {
            Llb_MtrSchedule( p->pMatrix );
            if ( pPars->fVerbose )
            {
                printf( "Matrix after scheduling:  " );
                Llb_MtrPrintMatrixStats( p->pMatrix );
                if ( pPars->fVeryVerbose )
                    Llb_MtrPrint( p->pMatrix, 1 );
            }
        }
    }
    
    if ( !p->pPars->fSkipReach ) 
        RetValue = Llb_ManReachability( p, vHints, pddGlo );
    Llb_ManStop( p );

    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );

    if ( pPars->fIndConstr )
        Vec_IntFreeP( &vHints );
    return RetValue;
}

int Llb_ManModelCheckGia	(	Gia_Man_t *	pGia,
		Gia_ParLlb_t *	pPars
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 197 of file llb1Core.c.

{
    Gia_Man_t * pGia2;
    Aig_Man_t * pAig;
    int RetValue = -1;
    pGia2 = Gia_ManDupDfs( pGia );
    pAig  = Gia_ManToAigSimple( pGia2 );
    Gia_ManStop( pGia2 );
//Aig_ManShow( pAig, 0, NULL ); 

    if ( pPars->nHintDepth == 0 )
        RetValue = Llb_ManModelCheckAig( pAig, pPars, NULL, NULL );
    else
        RetValue = Llb_ManModelCheckAigWithHints( pAig, pPars );
    pGia->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
    Aig_ManStop( pAig );
    return RetValue;
}

void Llb_ManPrintAig

(

Llb_Man_t *

p

)

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

Synopsis [Prints statistics about MFFCs.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file llb1Core.c.

{
    Abc_Print( 1, "pi =%3d  ",    Saig_ManPiNum(p->pAig) );
    Abc_Print( 1, "po =%3d  ",    Saig_ManPoNum(p->pAig) );
    Abc_Print( 1, "ff =%3d  ",    Saig_ManRegNum(p->pAig) );
    Abc_Print( 1, "int =%5d  ",   Vec_IntSize(p->vVar2Obj)-Aig_ManCiNum(p->pAig)-Saig_ManRegNum(p->pAig) );
    Abc_Print( 1, "var =%5d  ",   Vec_IntSize(p->vVar2Obj) );
    Abc_Print( 1, "part =%5d  ",  Vec_PtrSize(p->vGroups)-2 );
    Abc_Print( 1, "and =%5d  ",   Aig_ManNodeNum(p->pAig) );
    Abc_Print( 1, "lev =%4d  ",   Aig_ManLevelNum(p->pAig) );
//    Abc_Print( 1, "cut =%4d  ",   Llb_ManCrossCut(p->pAig) );
    Abc_Print( 1, "\n" );
}

ABC_NAMESPACE_IMPL_START void Llb_ManSetDefaultParams

(

Gia_ParLlb_t *

p

)

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