fsimSim.c File Reference

#include "fsimInt.h"
#include "aig/ssw/ssw.h"

Include dependency graph for fsimSim.c:

Go to the source code of this file.

Functions
void	Fsim_ManSimulateRoundTest (Fsim_Man_t *p)
Abc_Cex_t *	Fsim_ManGenerateCounter (Aig_Man_t *pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t *vCis2Ids)
int	Fsim_ManSimulate (Aig_Man_t *pAig, Fsim_ParSim_t *pPars)

Function Documentation

Fsim_ManGenerateCounter()

Abc_Cex_t * Fsim_ManGenerateCounter	(	Aig_Man_t *	pAig,
		int	iFrame,
		int	iOut,
		int	nWords,
		int	iPat,
		Vec_Int_t *	vCis2Ids )

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

Synopsis [Returns the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 433 of file fsimSim.c.

{
    Abc_Cex_t * p;
    unsigned * pData;
    int f, i, w, iPioId, Counter;
    p = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
    p->iFrame = iFrame;
    p->iPo = iOut;
    // fill in the binary data
    Aig_ManRandom( 1 );
    Counter = p->nRegs;
    pData = ABC_ALLOC( unsigned, nWords );
    for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
    for ( i = 0; i < Aig_ManPiNum(pAig); i++ )
    {
        iPioId = Vec_IntEntry( vCis2Ids, i );
        if ( iPioId >= p->nPis )
            continue;
        for ( w = nWords-1; w >= 0; w-- )
            pData[w] = Aig_ManRandom( 0 );
        if ( Aig_InfoHasBit( pData, iPat ) )
            Aig_InfoSetBit( p->pData, Counter + iPioId );
    }
    ABC_FREE( pData );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fsim_ManSimulate()

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

Here is the call graph for this function:

Fsim_ManSimulateRoundTest()

void Fsim_ManSimulateRoundTest

(

Fsim_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 384 of file fsimSim.c.

{
    Fsim_Obj_t * pObj;
    int i;
    clock_t clk = clock();
    Fsim_ManForEachObj( p, pObj, i )
    {
    }
//    ABC_PRT( "Unpacking time", p->pPars->nIters * (clock() - clk) );
}