saigSimSeq.c File Reference

#include "saig.h"
#include "proof/ssw/ssw.h"

Go to the source code of this file.

Data Structures
struct	Raig_Man_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Raig_Man_t_	Raig_Man_t
	DECLARATIONS ///. More...

Functions
static int	Raig_Var2Lit (int Var, int fCompl)
static int	Raig_Lit2Var (int Lit)
static int	Raig_LitIsCompl (int Lit)
static int	Raig_LitNot (int Lit)
static int	Raig_LitNotCond (int Lit, int c)
static int	Raig_LitRegular (int Lit)
int	Raig_ManFindPo (Aig_Man_t *pAig, int iNode)
	FUNCTION DEFINITIONS ///. More...
int	Raig_ManCreate_rec (Raig_Man_t *p, Aig_Obj_t *pObj)
Raig_Man_t *	Raig_ManCreate (Aig_Man_t *pAig)
void	Raig_ManDelete (Raig_Man_t *p)
unsigned *	Raig_ManSimRef (Raig_Man_t *p, int i)
unsigned *	Raig_ManSimDeref (Raig_Man_t *p, int i)
int	Raig_ManSimulateRound (Raig_Man_t *p, int fMiter, int fFirst, int *piPat)
Abc_Cex_t *	Raig_ManGenerateCounter (Aig_Man_t *pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t *vCis2Ids)
int	Raig_ManSimulate (Aig_Man_t *pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose)

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Raig_Man_t_ Raig_Man_t

DECLARATIONS ///.

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

FileName [saigSimSeq.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Sequential AIG package.]

Synopsis [Fast sequential AIG simulator.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]

Definition at line 32 of file saigSimSeq.c.

Function Documentation

static int Raig_Lit2Var ( int  Lit )

inlinestatic

Definition at line 62 of file saigSimSeq.c.

{ return Lit >> 1;           }

static int Raig_LitIsCompl ( int  Lit )

inlinestatic

Definition at line 63 of file saigSimSeq.c.

{ return Lit & 1;            }

static int Raig_LitNot ( int  Lit )

inlinestatic

Definition at line 64 of file saigSimSeq.c.

{ return Lit ^ 1;            }

static int Raig_LitNotCond ( int  Lit, int  c  )

inlinestatic

Definition at line 65 of file saigSimSeq.c.

{ return Lit ^ (int)(c > 0); }

static int Raig_LitRegular ( int  Lit )

inlinestatic

Definition at line 66 of file saigSimSeq.c.

{ return Lit & ~01;          }

Raig_Man_t* Raig_ManCreate

(

Aig_Man_t *

pAig

)

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

Synopsis [Creates fast simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 146 of file saigSimSeq.c.

{
    Raig_Man_t * p;
    Aig_Obj_t * pObj;
    int i, nObjs;
    Aig_ManCleanData( pAig );
    p = (Raig_Man_t *)ABC_ALLOC( Raig_Man_t, 1 );
    memset( p, 0, sizeof(Raig_Man_t) );
    p->pAig = pAig;
    p->nPis = Saig_ManPiNum(pAig);
    p->nPos = Saig_ManPoNum(pAig);
    p->nCis = Aig_ManCiNum(pAig);
    p->nCos = Aig_ManCoNum(pAig);
    p->nNodes = Aig_ManNodeNum(pAig);
    nObjs = p->nCis + p->nCos + p->nNodes + 2;
    p->pFans0 = ABC_ALLOC( int, nObjs );
    p->pFans1 = ABC_ALLOC( int, nObjs );
    p->pRefs = ABC_ALLOC( int, nObjs );
    p->pSims = ABC_CALLOC( unsigned, nObjs );
    p->vCis2Ids = Vec_IntAlloc( Aig_ManCiNum(pAig) );
    // add objects (0=unused; 1=const1)
    p->nObjs = 2;
    pObj = Aig_ManConst1( pAig );
    pObj->iData = 1;
    Aig_ManForEachCi( pAig, pObj, i )
        if ( Aig_ObjRefs(pObj) == 0 )
            Raig_ManCreate_rec( p, pObj );
    Aig_ManForEachCo( pAig, pObj, i )
        Raig_ManCreate_rec( p, pObj );
    assert( Vec_IntSize(p->vCis2Ids) == Aig_ManCiNum(pAig) );
    assert( p->nObjs == nObjs );
    // collect flop outputs
    p->vLos = Vec_IntAlloc( Aig_ManRegNum(pAig) );
    Saig_ManForEachLo( pAig, pObj, i )
        Vec_IntPush( p->vLos, pObj->iData );
    // collect flop inputs
    p->vLis = Vec_IntAlloc( Aig_ManRegNum(pAig) );
    Saig_ManForEachLi( pAig, pObj, i )
    {
        Vec_IntPush( p->vLis, pObj->iData );
        assert( p->pRefs[ pObj->iData ] == 0 );
        p->pRefs[ pObj->iData ]++;
    }
    return p;
}

int Raig_ManCreate_rec	(	Raig_Man_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Creates fast simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file saigSimSeq.c.

{
    int iFan0, iFan1;
    assert( !Aig_IsComplement(pObj) );
    if ( pObj->iData )
        return pObj->iData;
    assert( !Aig_ObjIsConst1(pObj) );
    if ( Aig_ObjIsNode(pObj) )
    {
        iFan0 = Raig_ManCreate_rec( p, Aig_ObjFanin0(pObj) );
        iFan0 = (iFan0 << 1) | Aig_ObjFaninC0(pObj);
        iFan1 = Raig_ManCreate_rec( p, Aig_ObjFanin1(pObj) );
        iFan1 = (iFan1 << 1) | Aig_ObjFaninC1(pObj);
    }
    else if ( Aig_ObjIsCo(pObj) )
    {
        iFan0 = Raig_ManCreate_rec( p, Aig_ObjFanin0(pObj) );
        iFan0 = (iFan0 << 1) | Aig_ObjFaninC0(pObj);
        iFan1 = 0;
    }
    else
    {
        iFan0 = iFan1 = 0;
        Vec_IntPush( p->vCis2Ids, Aig_ObjCioId(pObj) );
    }
    p->pFans0[p->nObjs] = iFan0;
    p->pFans1[p->nObjs] = iFan1;
    p->pRefs[p->nObjs] = Aig_ObjRefs(pObj);
    return pObj->iData = p->nObjs++;
}

void Raig_ManDelete

(

Raig_Man_t *

p

)

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

Synopsis [Creates fast simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 203 of file saigSimSeq.c.

{
    Vec_IntFree( p->vCis2Ids );
    Vec_IntFree( p->vLos );
    Vec_IntFree( p->vLis );
    ABC_FREE( p->pFans0 );
    ABC_FREE( p->pFans1 );
    ABC_FREE( p->pRefs );
    ABC_FREE( p->pSims );
    ABC_FREE( p->pMems );
    ABC_FREE( p );
}

int Raig_ManFindPo	(	Aig_Man_t *	pAig,
		int	iNode
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Find the PO corresponding to the PO driver.]

Description []

SideEffects []

SeeAlso []

Definition at line 83 of file saigSimSeq.c.

{
    Aig_Obj_t * pObj;
    int i;
    Saig_ManForEachPo( pAig, pObj, i )
        if ( pObj->iData == iNode )
            return i;
    return -1;
}

Abc_Cex_t* Raig_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 416 of file saigSimSeq.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_ManCiNum(pAig); i++ )
    {
        iPioId = Vec_IntEntry( vCis2Ids, i );
        if ( iPioId >= p->nPis )
            continue;
        for ( w = 0; w < nWords; w++ )
            pData[w] = Aig_ManRandom( 0 );
        if ( Abc_InfoHasBit( pData, iPat ) )
            Abc_InfoSetBit( p->pData, Counter + iPioId );
    }
    ABC_FREE( pData );
    return p;
}

unsigned* Raig_ManSimDeref	(	Raig_Man_t *	p,
		int	i
	)

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

Synopsis [Dereference simulaton info.]

Description []

SideEffects []

SeeAlso []

Definition at line 275 of file saigSimSeq.c.

{
    unsigned * pSim;
    assert( i );
    if ( i == 1 ) // const 1
        return p->pMems;
    assert( p->pSims[i] > 0 );
    pSim = p->pMems + p->pSims[i];
    if ( --pSim[0] == 0 )
    {
        pSim[0] = p->MemFree;
        p->MemFree = p->pSims[i];
        p->pSims[i] = 0;
        p->nMems--;
    }
    return pSim;
}

unsigned* Raig_ManSimRef	(	Raig_Man_t *	p,
		int	i
	)

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

Synopsis [References simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 227 of file saigSimSeq.c.

{
    unsigned * pSim;
    assert( i > 1 );
    assert( p->pSims[i] == 0 );
    if ( p->MemFree == 0 )
    {
        unsigned * pPlace, Ent;
        if ( p->nWordsAlloc == 0 )
        {
            assert( p->pMems == NULL );
            p->nWordsAlloc = (1<<17); // -> 1Mb
            p->nMems = 1;
        }
        p->nWordsAlloc *= 2;
        p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc );
        memset( p->pMems, 0xff, sizeof(unsigned) * (p->nWords + 1) );
        pPlace = (unsigned *)&p->MemFree;
        for ( Ent = p->nMems * (p->nWords + 1); 
              Ent + p->nWords + 1 < (unsigned)p->nWordsAlloc; 
              Ent += p->nWords + 1 )
        {
            *pPlace = Ent;
            pPlace = p->pMems + Ent;
        }
        *pPlace = 0;
    }
    p->pSims[i] = p->MemFree;
    pSim = p->pMems + p->MemFree;
    p->MemFree = pSim[0];
    pSim[0] = p->pRefs[i];
    p->nMems++;
    if ( p->nMemsMax < p->nMems )
        p->nMemsMax = p->nMems;
    return pSim;
}

int Raig_ManSimulate	(	Aig_Man_t *	pAig,
		int	nWords,
		int	nIters,
		int	TimeLimit,
		int	fMiter,
		int	fVerbose
	)

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

Synopsis [Returns 1 if the bug is detected, 0 otherwise.]

Description []

SideEffects []

SeeAlso []

Definition at line 454 of file saigSimSeq.c.

{
    Raig_Man_t * p;
    Sec_MtrStatus_t Status;
    int i, iPat, RetValue = 0;
    abctime clk, clkTotal = Abc_Clock();
    assert( Aig_ManRegNum(pAig) > 0 );
    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;
    }
    Aig_ManRandom( 1 );
    p = Raig_ManCreate( pAig );
    p->nWords = nWords;
    // iterate through objects
    for ( i = 0; i < nIters; i++ )
    {
        clk = Abc_Clock();
        RetValue = Raig_ManSimulateRound( p, fMiter, i==0, &iPat );
        if ( fVerbose )
        {
            printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, nIters, TimeLimit );
            printf("Time = %7.2f sec\r", (1.0*Abc_Clock()-clkTotal)/CLOCKS_PER_SEC);
        }
        if ( RetValue > 0 )
        {
            int iOut = Raig_ManFindPo(p->pAig, RetValue);
            assert( pAig->pSeqModel == NULL );
            pAig->pSeqModel = Raig_ManGenerateCounter( pAig, i, iOut, nWords, iPat, p->vCis2Ids );
            if ( fVerbose )
            printf( "Miter is satisfiable after simulation (output %d).\n", iOut );
            break;
        }
        if ( (Abc_Clock() - clk)/CLOCKS_PER_SEC >= TimeLimit )
        {
            printf( "No bug detected after %d frames with time limit %d seconds.\n", i+1, TimeLimit );
            break;
        }
    }
    if ( fVerbose )
    {
        printf( "Maxcut = %8d.  AigMem = %7.2f MB.  SimMem = %7.2f MB.  ", 
            p->nMemsMax, 
            1.0*(p->nObjs * 16)/(1<<20), 
            1.0*(p->nMemsMax * 4 * (nWords+1))/(1<<20) );
        ABC_PRT( "Total time", Abc_Clock() - clkTotal );
    }
    Raig_ManDelete( p );
    return RetValue > 0;
}

int Raig_ManSimulateRound	(	Raig_Man_t *	p,
		int	fMiter,
		int	fFirst,
		int *	piPat
	)

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

Synopsis [Simulates one round.]

Description [Returns the number of PO entry if failed; 0 otherwise.]

SideEffects []

SeeAlso []

Definition at line 304 of file saigSimSeq.c.

{ 
    unsigned * pRes0, * pRes1, * pRes;
    int i, w, nCis, nCos, iFan0, iFan1, iPioNum;
    // nove the values to the register outputs
    Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
    {
        if ( iPioNum < p->nPis )
            continue;
        pRes = Raig_ManSimRef( p, Vec_IntEntry(p->vLos, iPioNum-p->nPis) );
        if ( fFirst )
            memset( pRes + 1, 0, sizeof(unsigned) * p->nWords );
        else
        {
            pRes0 = Raig_ManSimDeref( p, Vec_IntEntry(p->vLis, iPioNum-p->nPis) );
            for ( w = 1; w <= p->nWords; w++ )
                pRes[w] = pRes0[w];
        }
        // handle unused PIs
        if ( pRes[0] == 0 ) 
        {
            pRes[0] = 1;
            Raig_ManSimDeref( p, Vec_IntEntry(p->vLos, iPioNum-p->nPis) );
        }
    }
    // simulate the logic
    nCis = nCos = 0;
    for ( i = 2; i < p->nObjs; i++ )
    {
        if ( p->pFans0[i] == 0 ) // ci always has zero first fanin
        {
            iPioNum = Vec_IntEntry( p->vCis2Ids, nCis );
            if ( iPioNum < p->nPis )
            {
                pRes = Raig_ManSimRef( p, i );
                for ( w = 1; w <= p->nWords; w++ )
                    pRes[w] = Aig_ManRandom( 0 );
                // handle unused PIs
                if ( pRes[0] == 0 ) 
                {
                    pRes[0] = 1;
                    Raig_ManSimDeref( p, i );
                }
            }
            else
                assert( Vec_IntEntry(p->vLos, iPioNum-p->nPis) == i );
            nCis++;
            continue;
        }
        if ( p->pFans1[i] == 0 ) // co always has non-zero 1st fanin and zero 2nd fanin
        {
            pRes0 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans0[i]) );
            if ( nCos < p->nPos && fMiter )
            {
                unsigned Const = Raig_LitIsCompl(p->pFans0[i])? ~0 : 0;
                for ( w = 1; w <= p->nWords; w++ )
                    if ( pRes0[w] != Const )
                    {
                        *piPat = 32*(w-1) + Aig_WordFindFirstBit( pRes0[w] ^ Const );
                        return i;
                    }
            }
            else
            {
                pRes = Raig_ManSimRef( p, i );
                assert( pRes[0] == 1 );
                if ( Raig_LitIsCompl(p->pFans0[i]) )
                    for ( w = 1; w <= p->nWords; w++ )
                        pRes[w] = ~pRes0[w];
                else
                    for ( w = 1; w <= p->nWords; w++ )
                        pRes[w] = pRes0[w];
            }
            nCos++;
            continue;
        }
        pRes  = Raig_ManSimRef( p, i );
        assert( pRes[0] > 0 );
        iFan0 = p->pFans0[i];
        iFan1 = p->pFans1[i];
        pRes0 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans0[i]) );
        pRes1 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans1[i]) );
        if ( Raig_LitIsCompl(iFan0) && Raig_LitIsCompl(iFan1) )
            for ( w = 1; w <= p->nWords; w++ )
                pRes[w] = ~(pRes0[w] | pRes1[w]);
        else if ( Raig_LitIsCompl(iFan0) && !Raig_LitIsCompl(iFan1) )
            for ( w = 1; w <= p->nWords; w++ )
                pRes[w] = ~pRes0[w] & pRes1[w];
        else if ( !Raig_LitIsCompl(iFan0) && Raig_LitIsCompl(iFan1) )
            for ( w = 1; w <= p->nWords; w++ )
                pRes[w] = pRes0[w] & ~pRes1[w];
        else if ( !Raig_LitIsCompl(iFan0) && !Raig_LitIsCompl(iFan1) )
            for ( w = 1; w <= p->nWords; w++ )
                pRes[w] = pRes0[w] & pRes1[w];
    }
    assert( nCis == p->nCis );
    assert( nCos == p->nCos );
    assert( p->nMems == 1 + Vec_IntSize(p->vLis) );
    return 0;
}

static int Raig_Var2Lit ( int  Var, int  fCompl  )

inlinestatic

Definition at line 61 of file saigSimSeq.c.

{ return Var + Var + fCompl; }