fsim.h File Reference

Go to the source code of this file.

Data Structures
struct	Fsim_ParSim_t_
struct	Fsim_ParSwitch_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Fsim_Man_t_	Fsim_Man_t
	INCLUDES ///. More...
typedef struct Fsim_ParSim_t_	Fsim_ParSim_t
typedef struct Fsim_ParSwitch_t_	Fsim_ParSwitch_t

Functions
void	Fsim_ManSetDefaultParamsSim (Fsim_ParSim_t *p)
	MACRO DEFINITIONS ///. More...
void	Fsim_ManSetDefaultParamsSwitch (Fsim_ParSwitch_t *p)
int	Fsim_ManSimulate (Aig_Man_t *pAig, Fsim_ParSim_t *pPars)
Vec_Int_t *	Fsim_ManSwitchSimulate (Aig_Man_t *pAig, Fsim_ParSwitch_t *pPars)
Vec_Ptr_t *	Fsim_ManTerSimulate (Aig_Man_t *pAig, int fVerbose)

Typedef Documentation

typedef typedefABC_NAMESPACE_HEADER_START struct Fsim_Man_t_ Fsim_Man_t

INCLUDES ///.

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

FileName [fsim.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Fast sequential AIG simulator.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]PARAMETERS ///BASIC TYPES ///

Definition at line 42 of file fsim.h.

typedef struct Fsim_ParSim_t_ Fsim_ParSim_t

Definition at line 45 of file fsim.h.

typedef struct Fsim_ParSwitch_t_ Fsim_ParSwitch_t

Definition at line 59 of file fsim.h.

Function Documentation

void Fsim_ManSetDefaultParamsSim

(

Fsim_ParSim_t *

p

)

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

MACRO DEFINITIONS ///.

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

FileName [fsimCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Fast sequential AIG simulator.]

Synopsis [Core procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file fsimCore.c.

{
    memset( p, 0, sizeof(Fsim_ParSim_t) );
    // user-controlled parameters
    p->nWords       =   8;    // the number of machine words
    p->nIters       =  32;    // the number of timeframes
    p->TimeLimit    =  60;    // time limit in seconds
    p->fCheckMiter  =   0;    // check if miter outputs are non-zero 
    p->fVerbose     =   1;    // enables verbose output
    // internal parameters
    p->fCompressAig =   0;    // compresses internal data
}

void Fsim_ManSetDefaultParamsSwitch

(

Fsim_ParSwitch_t *

p

)

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 69 of file fsimCore.c.

{
    memset( p, 0, sizeof(Fsim_ParSwitch_t) );
    // user-controlled parameters
    p->nWords       =   1;    // the number of machine words
    p->nIters       =  48;    // the number of timeframes
    p->nPref        =  16;    // the number of first timeframes to skip
    p->nRandPiNum   =   0;    // PI trans prob (0=1/2; 1=1/4; 2=1/8, etc)
    p->fProbOne     =   1;    // collect probability of one
    p->fProbTrans   =   1;    // collect probatility of switching
    p->fVerbose     =   1;    // enables verbose output
}

int Fsim_ManSimulate	(	Aig_Man_t *	pAig,
		Fsim_ParSim_t *	pPars
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 471 of file fsimSim.c.

{
    Fsim_Man_t * p;
    Sec_MtrStatus_t Status;
    int i, iOut, iPat;
    clock_t clk, clkTotal = clock(), clk2, clk2Total = 0;
    assert( Aig_ManRegNum(pAig) > 0 );
    if ( pPars->fCheckMiter )
    {
        Status = Sec_MiterStatus( pAig );
        if ( Status.nSat > 0 )
        {
            printf( "Miter is trivially satisfiable (output %d).\n", Status.iOut );
            return 1;
        }
        if ( Status.nUndec == 0 )
        {
            printf( "Miter is trivially unsatisfiable.\n" );
            return 0;
        }
    }
    // create manager
    clk = clock();
    p = Fsim_ManCreate( pAig );
    p->nWords = pPars->nWords;
    if ( pPars->fVerbose )
    {
        printf( "Obj = %8d (%8d). Cut = %6d. Front = %6d.  FrtMem = %7.2f MB. ", 
            p->nObjs, p->nCis + p->nNodes, p->nCrossCutMax, p->nFront, 
            4.0*p->nWords*(p->nFront)/(1<<20) );
        ABC_PRT( "Time", clock() - clk );
    }
    // create simulation frontier
    clk = clock();
    Fsim_ManFront( p, pPars->fCompressAig );
    if ( pPars->fVerbose )
    {
        printf( "Max ID = %8d. Log max ID = %2d.  AigMem = %7.2f MB (%5.2f byte/obj).  ", 
            p->iNumber, Aig_Base2Log(p->iNumber), 
            1.0*(p->pDataCur-p->pDataAig)/(1<<20), 
            1.0*(p->pDataCur-p->pDataAig)/p->nObjs ); 
        ABC_PRT( "Time", clock() - clk );
    }
    // perform simulation
    Aig_ManRandom( 1 );
    assert( p->pDataSim == NULL );
    p->pDataSim = ABC_ALLOC( unsigned, p->nWords * p->nFront );
    p->pDataSimCis = ABC_ALLOC( unsigned, p->nWords * p->nCis );
    p->pDataSimCos = ABC_ALLOC( unsigned, p->nWords * p->nCos );
    Fsim_ManSimInfoInit( p );
    for ( i = 0; i < pPars->nIters; i++ )
    { 
        Fsim_ManSimulateRound( p );
        if ( pPars->fVerbose )
        {
            printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
            printf( "Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC );
        }
        if ( pPars->fCheckMiter && Fsim_ManCheckPos( p, &iOut, &iPat ) )
        {
            assert( pAig->pSeqModel == NULL );
            pAig->pSeqModel = Fsim_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
            if ( pPars->fVerbose )
            printf( "Miter is satisfiable after simulation (output %d).\n", iOut );
            break;
        }
        if ( (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
            break;
        clk2 = clock();
        if ( i < pPars->nIters - 1 )
            Fsim_ManSimInfoTransfer( p );
        clk2Total += clock() - clk2;
    }
    if ( pAig->pSeqModel == NULL )
        printf( "No bug detected after %d frames with time limit %d seconds.\n", i+1, pPars->TimeLimit );
    if ( pPars->fVerbose )
    {
        printf( "Maxcut = %8d.  AigMem = %7.2f MB.  SimMem = %7.2f MB.  ", 
            p->nCrossCutMax, 
            p->pDataAig2? 12.0*p->nObjs/(1<<20) : 1.0*(p->pDataCur-p->pDataAig)/(1<<20), 
            4.0*p->nWords*(p->nFront+p->nCis+p->nCos)/(1<<20) );
        ABC_PRT( "Sim time", clock() - clkTotal );

//        ABC_PRT( "Additional time", clk2Total );
//        Fsim_ManSimulateRoundTest( p );
//        Fsim_ManSimulateRoundTest2( p );
    }
    Fsim_ManDelete( p );
    return pAig->pSeqModel != NULL;

}

Vec_Int_t* Fsim_ManSwitchSimulate	(	Aig_Man_t *	pAig,
		Fsim_ParSwitch_t *	pPars
	)

Vec_Ptr_t* Fsim_ManTerSimulate	(	Aig_Man_t *	pAig,
		int	fVerbose
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 339 of file fsimTsim.c.

{
    Fsim_Man_t * p;
    Vec_Ptr_t * vStates;
    unsigned ** pBins, * pState;
    int i, nWords, nBins;
    clock_t clk, clkTotal = clock();
    assert( Aig_ManRegNum(pAig) > 0 );
    // create manager
    clk = clock();
    p = Fsim_ManCreate( pAig );
    if ( fVerbose )
    {
        printf( "Obj = %8d (%8d). Cut = %6d. Front = %6d.  FrtMem = %7.2f MB. ", 
            p->nObjs, p->nCis + p->nNodes, p->nCrossCutMax, p->nFront, 
            4.0*Aig_BitWordNum(2 * p->nFront)/(1<<20) );
        ABC_PRT( "Time", clock() - clk );
    }
    // create simulation frontier
    clk = clock();
    Fsim_ManFront( p, 0 );
    if ( fVerbose )
    {
        printf( "Max ID = %8d. Log max ID = %2d.  AigMem = %7.2f MB (%5.2f byte/obj).  ", 
            p->iNumber, Aig_Base2Log(p->iNumber), 
            1.0*(p->pDataCur-p->pDataAig)/(1<<20), 
            1.0*(p->pDataCur-p->pDataAig)/p->nObjs ); 
        ABC_PRT( "Time", clock() - clk );
    }
    // allocate storage for terminary states
    nWords  = Abc_BitWordNum( 2*Aig_ManRegNum(pAig) );
    vStates = Vec_PtrAlloc( 1000 );
    nBins   = Abc_PrimeCudd( 500 );
    pBins   = ABC_ALLOC( unsigned *, nBins );
    memset( pBins, 0, sizeof(unsigned *) * nBins );
    // perform simulation
    assert( p->pDataSim == NULL );
    p->pDataSim = ABC_ALLOC( unsigned, Aig_BitWordNum(2 * p->nFront) * sizeof(unsigned) );
    p->pDataSimCis = ABC_ALLOC( unsigned, Aig_BitWordNum(2 * p->nCis) * sizeof(unsigned) );
    p->pDataSimCos = ABC_ALLOC( unsigned, Aig_BitWordNum(2 * p->nCos) * sizeof(unsigned) );
    Fsim_ManTerSimInfoInit( p );
    // hash the first state
    pState = Fsim_ManTerStateCreate( p->pDataSimCis, p->nPis, p->nCis, nWords );
    Vec_PtrPush( vStates, pState );
    Fsim_ManTerStateInsert( pState, nWords, pBins, nBins );
    // perform simuluation till convergence
    for ( i = 0; ; i++ )
    {
        Fsim_ManTerSimulateRound( p );
        Fsim_ManTerSimInfoTransfer( p );
        // hash the first state
        pState = Fsim_ManTerStateCreate( p->pDataSimCis, p->nPis, p->nCis, nWords );
        Vec_PtrPush( vStates, pState );
        if ( Fsim_ManTerStateLookup(pState, nWords, pBins, nBins) )
            break;
        Fsim_ManTerStateInsert( pState, nWords, pBins, nBins );
    }
    if ( fVerbose )
    {
        printf( "Maxcut = %8d.  AigMem = %7.2f MB.  SimMem = %7.2f MB.  ", 
            p->nCrossCutMax, 
            p->pDataAig2? 12.0*p->nObjs/(1<<20) : 1.0*(p->pDataCur-p->pDataAig)/(1<<20), 
            4.0*(Aig_BitWordNum(2 * p->nFront)+Aig_BitWordNum(2 * p->nCis)+Aig_BitWordNum(2 * p->nCos))/(1<<20) );
        ABC_PRT( "Sim time", clock() - clkTotal );
    }
    ABC_FREE( pBins );
    Fsim_ManDelete( p );
    return vStates;

}