sswRarity2.c File Reference

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

Include dependency graph for sswRarity2.c:

Go to the source code of this file.

Classes
struct	Ssw_RarMan_t_

Functions
int	Ssw_RarSimulate2 (Aig_Man_t *pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose)
int	Ssw_RarSignalFilter2 (Aig_Man_t *pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t *pCex, int fLatchOnly, int fVerbose)
int	Ssw_RarSignalFilterGia2 (Gia_Man_t *p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t *pCex, int fLatchOnly, int fVerbose)

Function Documentation

Ssw_RarSignalFilter2()

int Ssw_RarSignalFilter2	(	Aig_Man_t *	pAig,
		int	nFrames,
		int	nWords,
		int	nBinSize,
		int	nRounds,
		int	TimeOut,
		Abc_Cex_t *	pCex,
		int	fLatchOnly,
		int	fVerbose )

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

Synopsis [Filter equivalence classes of nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 386 of file sswRarity2.c.

{
    int fMiter = 0;
    Ssw_RarMan_t * p;
    int r, i, k;
    abctime clkTotal = Abc_Clock();
    abctime nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
    int RetValue = -1;
    assert( Aig_ManRegNum(pAig) > 0 );
    assert( Aig_ManConstrNum(pAig) == 0 );
    // consider the case of empty AIG
    if ( Aig_ManNodeNum(pAig) == 0 )
        return -1;
    if ( fVerbose )
        Abc_Print( 1, "Filtering equivs with %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n",
            nWords, nFrames, nBinSize, nRounds, TimeOut );
    // reset random numbers
    Aig_ManRandom( 1 );
 
    // create manager
    p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
    // compute starting state if needed
    assert( p->vInits == NULL );
    if ( pCex )
        p->vInits = Ssw_RarFindStartingState( pAig, pCex );
    else
        p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) );
    // duplicate the array
    for ( i = 1; i < nWords; i++ )
        for ( k = 0; k < Aig_ManRegNum(pAig); k++ )
            Vec_IntPush( p->vInits, Vec_IntEntry(p->vInits, k) );
    assert( Vec_IntSize(p->vInits) == Aig_ManRegNum(pAig) * nWords );
    // initialize simulation manager
    Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
 
    // create trivial equivalence classes with all nodes being candidates for constant 1
    if ( pAig->pReprs == NULL )
        p->ppClasses = Ssw_ClassesPrepareSimple( pAig, fLatchOnly, 0 );
    else
        p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig );
    Ssw_ClassesSetData( p->ppClasses, p->pSml, NULL, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
    // print the stats
    if ( fVerbose )
    {
        Abc_Print( 1, "Initial  :  " );
        Ssw_ClassesPrint( p->ppClasses, 0 );
    }
    // refine classes using BMC
    for ( r = 0; r < nRounds; r++ )
    {
        // start filtering equivalence classes
        if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 )
        {
            Abc_Print( 1, "All equivalences are refined away.\n" );
            break;
        }
        // simulate
        Ssw_SmlSimulateOne( p->pSml );
        if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
        {
            if ( fVerbose ) Abc_Print( 1, "\n" );
            Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
            RetValue = 0;
            break;
        }
        // check equivalence classes
        Ssw_ClassesRefineConst1( p->ppClasses, 1 );
        Ssw_ClassesRefine( p->ppClasses, 1 );
        // printout
        if ( fVerbose )
        {
            Abc_Print( 1, "Round %3d:  ", r );
            Ssw_ClassesPrint( p->ppClasses, 0 );
        }
        // get initialization patterns
        Ssw_RarUpdateCounters( p );
        Ssw_RarTransferPatterns( p, p->vInits );
        Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
        // check timeout
        if ( TimeOut && Abc_Clock() > nTimeToStop )
        {
            if ( fVerbose ) Abc_Print( 1, "\n" );
            Abc_Print( 1, "Reached timeout (%d seconds).\n",  TimeOut );
            break;
        }
    }
    if ( r == nRounds )
    {
        Abc_Print( 1, "Simulation did not assert POs in the first %d frames.  ", nRounds * nFrames );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
    }
    // cleanup
    Ssw_RarManStop( p );
    return -1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_RarSignalFilterGia2()

int Ssw_RarSignalFilterGia2	(	Gia_Man_t *	p,
		int	nFrames,
		int	nWords,
		int	nBinSize,
		int	nRounds,
		int	TimeOut,
		Abc_Cex_t *	pCex,
		int	fLatchOnly,
		int	fVerbose )

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

Synopsis [Filter equivalence classes of nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 493 of file sswRarity2.c.

{
    Aig_Man_t * pAig;
    int RetValue;
    pAig = Gia_ManToAigSimple( p );
    if ( p->pReprs != NULL )
    {
        Gia_ManReprToAigRepr2( pAig, p );
        ABC_FREE( p->pReprs );
        ABC_FREE( p->pNexts );
    }
    RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose );
    Gia_ManReprFromAigRepr( pAig, p );
    Aig_ManStop( pAig );
    return RetValue;
}

Here is the call graph for this function:

Ssw_RarSimulate2()

int Ssw_RarSimulate2	(	Aig_Man_t *	pAig,
		int	nFrames,
		int	nWords,
		int	nBinSize,
		int	nRounds,
		int	TimeOut,
		int	fVerbose )

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

Synopsis [Perform sequential simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file sswRarity2.c.

{
    int fMiter = 1;
    Ssw_RarMan_t * p;
    int r;
    abctime clk, clkTotal = Abc_Clock();
    abctime nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
    int RetValue = -1;
    assert( Aig_ManRegNum(pAig) > 0 );
    assert( Aig_ManConstrNum(pAig) == 0 );
    // consider the case of empty AIG
    if ( Aig_ManNodeNum(pAig) == 0 )
        return -1;
    if ( fVerbose )
        Abc_Print( 1, "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n",
            nWords, nFrames, nBinSize, nRounds, TimeOut );
    // reset random numbers
    Aig_ManRandom( 1 );
 
    // create manager
    p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
    p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords );
    Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
 
    // perform simulation rounds
    for ( r = 0; r < nRounds; r++ )
    {
        clk = Abc_Clock();
        // simulate
        Ssw_SmlSimulateOne( p->pSml );
        if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
        {
            if ( fVerbose ) Abc_Print( 1, "\n" );
            Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
            RetValue = 0;
            break;
        }
        // get initialization patterns
        Ssw_RarUpdateCounters( p );
        Ssw_RarTransferPatterns( p, p->vInits );
        Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
        // printout
        if ( fVerbose )
        {
//            Abc_Print( 1, "Round %3d:  ", r );
//            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
            Abc_Print( 1, "." );
        }
        // check timeout
        if ( TimeOut && Abc_Clock() > nTimeToStop )
        {
            if ( fVerbose ) Abc_Print( 1, "\n" );
            Abc_Print( 1, "Reached timeout (%d seconds).\n",  TimeOut );
            break;
        }
    }
    if ( r == nRounds )
    {
        if ( fVerbose ) Abc_Print( 1, "\n" );
        Abc_Print( 1, "Simulation did not assert POs in the first %d frames.  ", nRounds * nFrames );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
    }
    // cleanup
    Ssw_RarManStop( p );
    return RetValue;
}

Here is the call graph for this function: